aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tauto.ml4
Commit message (Expand)AuthorAge
* 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
* Message d'erreur plus explicite pour TautoGravatar delahaye2001-02-05
* rétablissement nouveau TautoGravatar filliatr2001-02-05
* Résolution d'un bug de simplificationGravatar delahaye2001-02-03
* oubli de Closure.EvalConstRefGravatar filliatr2001-02-01
* - coqc : option -imageGravatar filliatr2001-02-01
* Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_mainGravatar sacerdot2001-01-30
* As an heuristic, now both in tauto and intuition we try to avoid the initialGravatar sacerdot2001-01-29
* Elimination du 'Gravatar delahaye2000-11-28
* Nouveau choix pour l'intros initialGravatar delahaye2000-11-24
* On n'introduit que des produits non dependantsGravatar delahaye2000-11-23
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
* Remplacement de Tauto et IntuitionGravatar delahaye2000-10-30