aboutsummaryrefslogtreecommitdiff
path: root/tactics/auto.ml
AgeCommit message (Collapse)Author
2003-11-13factorisation et generalisation des clausesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTac; localisation des appels à des tactiques ↵herbelin
définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3824 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Option pour rendre les vérifications du refiner optionnelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Vraie substitutivite de autohintscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27passage a ocaml 3.06herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3041 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13Renoncement à distinguer les types "constr" et "types"; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2963 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Nouveau Rewrite-in plus economiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15petits changements cosmetiques sur les tactiquesbarras
+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-11substitution et pattern modulo letbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-28Change la constante d'entree de Immediatemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1901 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-31Amelioration - subjective - de l'affichage des Hintherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1774 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16Prise en compte noms longs dans SuperAutoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1391 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en ↵herbelin
compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1388 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et ↵herbelin
réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce ↵herbelin
dernier qui échouera si c'est pas normalisé de tête git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1218 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Normalisation betaiota du pattern avant enregistrement comme hint (certains ↵herbelin
développements exploite cette caractéristique) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1214 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12Hint Unfold Local + commentairesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1088 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon ↵filliatr
Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@923 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15methode exportfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans ↵herbelin
library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@839 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-02suppression des (* open Generic *)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec ↵herbelin
sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Renommage canonique :herbelin
declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-13Suppression du test de convertibilite inutile pour la plupart des exact; 2 ↵herbelin
versions exact_no_check, exact_check git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@705 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de l'env local dans make_apply_entryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@685 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Mise en page de Print Hintherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@670 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Abstraction de constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Correction pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@590 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Modifs d'interpretation de patternsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@562 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-28Modifs de presentation.delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@520 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 18:27:04 +0000