#
f9642e8e |
|
28-Apr-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Rename match_all_tac to first_match_tac The new name is less confusing, given what it does. Arguably it does not need to be bound at all, since the implementation is so simple.
|
#
bb599ff9 |
|
18-Apr-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Simplify match_goal.sig So there is only one main signature in the file, to make things easier with Moscow ML, as suggested by Michael.
|
#
2c54b95f |
|
13-Apr-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Remove string-based encoding of names, tidy signature The preferred approach to creating matchers is via the mg structure, so there is no need for a hacky string-based approach to short names.
|
#
705eb764 |
|
09-Apr-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Add an initial implementation of match_goal This is a tactic builder that does automatic logic-programming-style search over (sub)terms in the assumptions and conclusion of a goal ensuring certain patterns match and that a given tactic (which can refer to the terms and assumptions named by the pattern) succeeds. Work with Jack Gallagher, and inspired by a similar facility in Coq.
|