aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tauto.ml4
Commit message (Expand)AuthorAge
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* Fixed a hole in glob_tactic that allowed some Ltac code to refer toGravatar herbelin2009-09-26
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Fix tauto no longer failing after commit 12077; appropriate errorGravatar herbelin2009-04-10
* Turning tauto into a classical tautology prover as soon as classicalGravatar herbelin2009-04-09
* Solves some warning and hides some not-bad ones in doc. It remains aGravatar herbelin2009-01-29
* - Fixed bugs and compatibilities issues in Gravatar herbelin2008-12-30
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* More compatibility fixes, revert the tauto fix that preventedGravatar msozeau2008-07-25
* Tauto breaking not only binary "conjunctions" seems like a bad ideaGravatar msozeau2008-07-24
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Modifications diverses et variées :Gravatar herbelin2008-03-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Nouvelle en-têteGravatar herbelin2004-07-16
* *** empty log message ***Gravatar barras2003-12-23
* petits changements de syntaxeGravatar barras2003-11-12
* nouvelle syntaxe de ltacGravatar barras2003-10-16
* Passage à la V8 par défautGravatar herbelin2003-09-22
* switching back to old tautoGravatar corbinea2003-07-03
* added hints into GroundGravatar corbinea2003-07-02
* *** empty log message ***Gravatar courant2003-06-27
* Preservation affichage des ?n en V7Gravatar herbelin2003-05-22
* Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...Gravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* Fixed Relative names not,iff in Camlp4 quotation.Gravatar corbinea2003-03-28
* Introducing Christine's Intuition1 and adding some invertible hyps.Gravatar corbinea2003-03-18
* Changed Tauto so it displays less 'Unfold not iff'Gravatar corbinea2003-02-26
* Suppression de l'élimination des existentiels dans LinearIntuition.Gravatar corbinea2003-02-05
* Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).Gravatar corbinea2003-01-23
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* correction bugs TautoGravatar courant2002-07-19
* Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3|- ?]Gravatar corbinea2002-07-17
* Correction bug Tauto : la regle pour (A->B)->C echouait quand C etaitGravatar courant2002-07-15
* NettoyageGravatar herbelin2002-05-30
* Fichiers tactics/*.ml4 remplacent les tactics/*.vGravatar herbelin2002-05-29
* Correction of a bug in Intuition (no more decomposition of dependent pairs).Gravatar corbinea2002-05-22
* Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deGravatar herbelin2002-05-15
* Finalement VTactic est gardé pour y plonger les tactiques ML, leGravatar herbelin2002-05-15
* - Changement de l'ordre de filtrage dans "Match Context"Gravatar herbelin2002-05-14
* nettoyage codeGravatar courant2002-05-02
* *** empty log message ***Gravatar courant2002-04-08
* Intuition ne fait plus de Unfold des constantes (il faut les faireGravatar courant2002-03-21