aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
* Nouveau long long avec Coq en têteGravatar herbelin2000-11-29
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* Elimination du 'Gravatar delahaye2000-11-28
* Prise en compte des let-in dans les fonctions de réduction pour les tactiquesGravatar herbelin2000-11-27
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...Gravatar herbelin2000-11-26
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* Nouveau choix pour l'intros initialGravatar delahaye2000-11-24
* On n'introduit que des produits non dependantsGravatar delahaye2000-11-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 12:02:07 +0000