aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tauto.ml4
Commit message (Expand)AuthorAge
* *** 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
* Intuition now takes an (optional) tactic as parameter. This tactic isGravatar courant2002-03-20
* Tauto est maintenant stable par "Intro" :Gravatar courant2002-03-15
* substitution et pattern modulo letGravatar barras2002-02-11
* Mise en place de la réduction sous forme d'implications d'atomes en fn de têteGravatar herbelin2001-12-20
* Utilisation de Hnf plutôt que RedGravatar herbelin2001-12-20
* Puisque Orelse semble lier moins que THEN, ajout d'un reduce après le OrelseGravatar herbelin2001-12-19
* Insertion de Red sur chaque atome dans Tauto et IntuitionGravatar herbelin2001-12-19
* Tentative d'amélioration du résultat de IntuitionGravatar herbelin2001-12-19
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRGravatar delahaye2001-10-23
* Ajout du printer de tactiques + modif du Dynamic ocamlGravatar delahaye2001-09-30
* ParsingGravatar herbelin2001-08-10
* Modification Tauto pour qu'il puisse destructurer des hypotheses de la formeGravatar courant2001-08-08
* Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...Gravatar herbelin2001-06-25
* Fix d'un bug de TautoGravatar delahaye2001-06-15
* Correction d'un bug du a un Intros trop violentGravatar delahaye2001-06-01
* Ajout du cas True->A|-BGravatar delahaye2001-04-24
* entetesGravatar filliatr2001-03-15
* Ajout d'une heuristique pour les types dependantsGravatar delahaye2001-02-05