aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
2001-03-01backtrack unification types et deplacement make_clenv_bindingfilliatr
2001-02-26changement message d'erreur Abstractfilliatr
2001-02-26Abstract: on échoue si le but contient des existentiellesfilliatr
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...herbelin
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des const...filliatr
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2000-12-26On n'évite plus les globaux dans Intro, mais on les évite dans Abstractherbelin
2000-12-25Retrait du test d'existence "is_global" dans Intro ( fresh_id ) dherbelin
2000-12-20Toujours Inductionherbelin
2000-12-20Toujours Inductionherbelin
2000-12-20Induction/NewInductionherbelin
2000-12-18Renommages autour de NewInductionherbelin
2000-12-12Hint Unfold Local + commentairesmohring
2000-12-12Reparation Intro sans nom qui ne reduisait pas le but quand celui-cimohring
2000-12-06message d'erreurherbelin
2000-12-06Divers bugs LetTacherbelin
2000-12-04caractere opaque des constantes repris en comptefilliatr
2000-12-02Portage d'AutoRewritedelahaye
2000-11-29Nouveau long long avec Coq en têteherbelin
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath po...herbelin
2000-11-26Appel des constantes globaux par des noms absolusherbelin
2000-11-26Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...herbelin
2000-11-24Nouveau choix pour l'intros initialdelahaye
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...herbelin
2000-11-20Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...herbelin
2000-11-09Bug et simplification nouvel Inductionherbelin
2000-11-07Nettoyage Names suiteherbelin
2000-11-06Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; bah.....herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-27erreur dans intro_gen corrigéefilliatr
2000-10-27Intro choue si le nom d'hypothse existe au lieu de mettre un avertissementherbelin
2000-10-18Renommage canonique :herbelin
2000-10-13Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...herbelin
2000-10-05Bug de conflit de nommage d'hyp d'induction dans l'Induction fonctionnant dan...herbelin
2000-10-03Rebranchement de la tactique Letherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Plus de whd_castapp_stackherbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-28messages d'erreurherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-06-29Rienherbelin
2000-05-25Déplacement de save_thm and co de PFedit vers Commandherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:48:48 +0000