aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/setoid_replace.ml
Commit message (Expand)AuthorAge
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
* *** empty log message ***Gravatar barras2003-03-12
* Correction bug réecriture à la racine pour le sétoide Prop.Gravatar clrenard2003-01-22
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et LocalGravatar herbelin2002-10-23
* bug de noms long pour eqT.Gravatar clrenard2002-10-01
* Que des niveaux d'univers frais dans le type des constantes globalesGravatar herbelin2002-09-29
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Changement de eq en eqT comme equivalence de setoide par defaut.Gravatar clrenard2002-05-14
* Minor correction of get_lem_nameGravatar coq2002-05-02
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* TransparentGravatar barras2001-09-20
* Deplacement des setoides.Gravatar clrenard2001-09-19
* Modification de l'emplacement des fichiers pour les setoides.Gravatar clrenard2001-09-18
* ParsingGravatar herbelin2001-08-10
* Ajout du .ml pour la tactique Setoid_replaceGravatar clrenard2001-07-10