aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extratactics.ml4
Commit message (Expand)AuthorAge
* New commandsGravatar sacerdot2004-10-07
* * New syntactic sugar: Add Relation ... transitivity proved by ...Gravatar sacerdot2004-10-06
* The "Add Setoid" command now has a new argument "as name" that is usedGravatar sacerdot2004-10-01
* New tacticGravatar sacerdot2004-09-30
* New tactic [setoid_]rewrite ... in ... [generate side conditions ...].Gravatar sacerdot2004-09-30
* cutrewrite does not work with relations that are not Coq-like equalities.Gravatar sacerdot2004-09-30
* New syntaxGravatar sacerdot2004-09-29
* Hugly temporary notationGravatar sacerdot2004-09-29
* New: (temporary) concrete syntax to specify the morphism signature:Gravatar sacerdot2004-09-24
* Add_new_morphism has now a new optional argument that is the signature ofGravatar sacerdot2004-09-10
* New command "Add Relation ..." (for the new implementation of setoid_*).Gravatar sacerdot2004-09-03
* Setoid_replace.setoid_replace last argument (that was supposed to be alwaysGravatar sacerdot2004-07-23
* Nouvelle en-têteGravatar herbelin2004-07-16
* syntax compatibility fixGravatar corbinea2004-07-02
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* more evar stuffGravatar corbinea2004-06-28
* Backtrack sur commit 1.20Gravatar herbelin2004-03-18
* Desactivation de la syntaxe v7 de Hint Rewrite en v8Gravatar herbelin2004-03-17
* Ajout tactiques stepl et stepr de NimègueGravatar herbelin2004-03-10
* Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...Gravatar herbelin2004-03-02
* Ajout 'replace in'Gravatar herbelin2004-03-01
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* petits changements de syntaxeGravatar barras2003-11-12
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
* Extension de l'utilisation de contradictionGravatar herbelin2003-10-19
* Cablage en dur de inversionGravatar herbelin2003-10-10
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
* *** empty log message ***Gravatar barras2003-03-12
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Subst (tout court)Gravatar filliatr2002-09-16
* tactique Subst x1 ... xnGravatar filliatr2002-09-11
* tactique SubstGravatar filliatr2002-07-17
* Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...Gravatar herbelin2002-06-05
* Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...Gravatar herbelin2002-06-05
* Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...Gravatar herbelin2002-06-05
* Fichiers tactics/*.ml4 remplacent les tactics/*.vGravatar herbelin2002-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:56:25 +0000