aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* nouvelle implantation de la reductionGravatar barras2001-03-01
* modifGravatar mohring2001-02-28
* EAuto mixte (largeur puis profondeur)Gravatar mohring2001-02-27
* changement message d'erreur AbstractGravatar filliatr2001-02-26
* Eauto version en largeurGravatar mohring2001-02-26
* Abstract: on échoue si le but contient des existentiellesGravatar filliatr2001-02-26
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Prise en compte noms longs dans SuperAutoGravatar herbelin2001-02-16
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* Bug affichageGravatar herbelin2001-02-14
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* code mortGravatar herbelin2001-02-07
* EqDecideGravatar filliatr2001-02-06
* 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
* application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésGravatar filliatr2001-02-01
* oubli de Closure.EvalConstRefGravatar filliatr2001-02-01
* - coqc : option -imageGravatar filliatr2001-02-01
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* 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
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* On n'évite plus les globaux dans Intro, mais on les évite dans AbstractGravatar herbelin2000-12-26
* Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce der...Gravatar herbelin2000-12-26
* Command -> ConstrGravatar herbelin2000-12-25
* Retrait du test d'existence "is_global" dans Intro ( fresh_id ) dGravatar herbelin2000-12-25
* Normalisation betaiota du pattern avant enregistrement comme hint (certains d...Gravatar herbelin2000-12-25
* Bug confusion existS/sigSGravatar herbelin2000-12-25
* Command -> ConstrGravatar herbelin2000-12-25
* Toujours InductionGravatar herbelin2000-12-20
* Toujours InductionGravatar herbelin2000-12-20
* Induction/NewInductionGravatar herbelin2000-12-20
* AutoRewrite n'ecrit plus de valeurs fonctionnelles sur disqueGravatar delahaye2000-12-19
* Renommages autour de NewInductionGravatar herbelin2000-12-18
* suppression warning et calcule type dans replace_by_meta dans tous les casGravatar filliatr2000-12-15
* LetIn dans SimplGravatar mohring2000-12-14
* Bug Inversion en présence de méta-variablesGravatar herbelin2000-12-13
* conflit useInversionLemmaGravatar mohring2000-12-13
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* Reparation Intro sans nom qui ne reduisait pas le but quand celui-ciGravatar mohring2000-12-12
* message d'erreurGravatar herbelin2000-12-06
* Divers bugs LetTacGravatar herbelin2000-12-06
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* Portage d'AutoRewriteGravatar delahaye2000-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-05 04:43:48 +0000