aboutsummaryrefslogtreecommitdiff
path: root/tactics/tauto.ml4
AgeCommit message (Expand)Author
2001-08-10Parsingherbelin
2001-08-08Modification Tauto pour qu'il puisse destructurer des hypotheses de la formecourant
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...herbelin
2001-06-15Fix d'un bug de Tautodelahaye
2001-06-01Correction d'un bug du a un Intros trop violentdelahaye
2001-04-24Ajout du cas True->A|-Bdelahaye
2001-03-15entetesfilliatr
2001-02-05Ajout d'une heuristique pour les types dependantsdelahaye
2001-02-05Message d'erreur plus explicite pour Tautodelahaye
2001-02-05rétablissement nouveau Tautofilliatr
2001-02-03Résolution d'un bug de simplificationdelahaye
2001-02-01oubli de Closure.EvalConstReffilliatr
2001-02-01- coqc : option -imagefilliatr
2001-01-30Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_mainsacerdot
2001-01-29As an heuristic, now both in tauto and intuition we try to avoid the initialsacerdot
2000-11-28Elimination du 'delahaye
2000-11-24Nouveau choix pour l'intros initialdelahaye
2000-11-23On n'introduit que des produits non dependantsdelahaye
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
2000-10-30Remplacement de Tauto et Intuitiondelahaye
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 08:44:56 +0000