aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne p...Gravatar herbelin2001-07-13
* Autoriser Apply avec un but sous forme d'implication ou de quantificationGravatar barras2001-06-29
* traitement du let dans red_product (tactique Red)Gravatar barras2001-06-29
* commit d'un bug de Apply.Gravatar barras2001-06-27
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* Prise en compte env local (et defs locales) dans ChangeGravatar herbelin2001-06-13
* Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ...Gravatar herbelin2001-06-01
* Mis un message d'erreur explicite pour l'echec de Elim en casGravatar mohring2001-04-12
* Make it possible to perform proofs by induction even on non-inductive types,Gravatar bertot2001-04-03
* amelioration de la structure des universGravatar barras2001-03-28
* Problèmes de NewInductionGravatar herbelin2001-03-22
* entetesGravatar filliatr2001-03-15
* backtrack unification types et deplacement make_clenv_bindingGravatar filliatr2001-03-01
* changement message d'erreur AbstractGravatar filliatr2001-02-26
* Abstract: on échoue si le but contient des existentiellesGravatar filliatr2001-02-26
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* On n'évite plus les globaux dans Intro, mais on les évite dans AbstractGravatar herbelin2000-12-26
* Retrait du test d'existence "is_global" dans Intro ( fresh_id ) dGravatar herbelin2000-12-25
* Toujours InductionGravatar herbelin2000-12-20
* Toujours InductionGravatar herbelin2000-12-20
* Induction/NewInductionGravatar herbelin2000-12-20
* Renommages autour de NewInductionGravatar herbelin2000-12-18
* 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
* 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
* Nouveau choix pour l'intros initialGravatar delahaye2000-11-24
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* Bug et simplification nouvel InductionGravatar herbelin2000-11-09
* Nettoyage Names suiteGravatar herbelin2000-11-07
* Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; bah.....Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* erreur dans intro_gen corrigéeGravatar filliatr2000-10-27
* Intro choue si le nom d'hypothse existe au lieu de mettre un avertissementGravatar herbelin2000-10-27
* Renommage canonique :Gravatar herbelin2000-10-18
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* Bug de conflit de nommage d'hyp d'induction dans l'Induction fonctionnant dan...Gravatar herbelin2000-10-05
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
* Renommage AppL en AppGravatar herbelin2000-10-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-16 10:14:03 +0000