aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* amelioration de la structure des universGravatar barras2001-03-28
* Problèmes de NewInductionGravatar herbelin2001-03-22
* entetesGravatar filliatr2001-03-15
* bug de refine: uncaught exception Array.subGravatar barras2001-03-09
* changement comparaison etatsGravatar filliatr2001-03-08
* Modification de e_give_exact pour eviter d'echouer sur l'unificationGravatar mohring2001-03-06
* eta-expansionGravatar mohring2001-03-06
* EAutod (debug)Gravatar filliatr2001-03-06
* module Explore générique et réécriture EAuto avec ce module; occur check ...Gravatar filliatr2001-03-05
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* backtrack unification types et deplacement make_clenv_bindingGravatar filliatr2001-03-01
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 15:10:32 +0000