aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.mli
Commit message (Collapse)AuthorAge
...
* Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrageGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
| | | | | | | | | Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de type_of_case, type_case_branches, etc;nettoyageGravatar herbelin2000-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@350 85f007b7-540e-0410-9357-904b9bb8a0f7
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7