aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_tactic.ml4
AgeCommit message (Collapse)Author
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2735 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-19Ajout de l'entrée ne_constrarg_listdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2543 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-01Ajout tactiques Rename et Pose; modifications pour Inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2449 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-31changement generation de schema d'elimination, False_rec est primitif, ↵mohring
Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 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-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs ↵herbelin
'ClearBody H' et 'Assert H := c' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14Ajout syntaxe "Assert H:T."herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1968 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-28Remplace numarg -> pure_numarg dans Double Inductionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1900 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Parsingherbelin
- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08Renommage TrueCut -> Assertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1887 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ↵herbelin
tactique primitive Cut basé sur un Let non dépendant; amélioration efficacité ancien Cut git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1883 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Mise en place d'un nouveau Destruct sur le modèle du nouvel Inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1874 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans ↵herbelin
Compute, nouveaux flags utilisateurs pour Evar et Zeta git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1820 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵herbelin
définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵herbelin
compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-19Extension des parametres de Clear + Instdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1794 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-18Interpretation MetaId + Progress + Instdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1789 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-11Fix de quelques bugs syntaxiques de Ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1780 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Les clauses de Rec doivent prendre des tactic_atom'sdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1701 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Petit menagedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1642 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19*** empty log message ***mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1610 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Essais dans Ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1606 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-14Non parenthesage des applications de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1590 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-12Ajout de _ dans les patterns d'intromohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1584 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug ↵filliatr
d'ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 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-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-07Modif pour les patterns de sous-termesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1347 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1307 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des ↵filliatr
constantes qualifiees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1301 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20ajout ident_or_constrarg pour NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1167 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Correction associativite de Repeat/Orelsedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1151 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-11numarg -> pure_numarg a poursuivremohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1084 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Extension de la syntaxe de LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1068 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Correction pour les qualidconstargdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1056 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Plus de quote devant les ident et les ?delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1054 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Elimination du 'delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Distinction claire entre Induction (nom interne : raw_induct) et le nouvel ↵herbelin
induction (now temporaire NewInduction) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@960 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Bug qualidconstarg (intervient pour Transparent)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@921 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Nouvelle entrée qualidarg pour noms qualifiés; nouveau lexeme METAIDENT ↵herbelin
pour les $id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@880 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@795 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-30Priorite du Try/Orelse + Debug switch + correction bug dans Patterndelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@785 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Ajout castedopenconstrarg; Renommage tactique Let en LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@640 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-08-17Pattern matching de sous-termes + exceptions dans le lexerdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@578 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Modifs d'interpretation de patterns + exceptions dans le lexerdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@561 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Ajout du langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:37:37 +0000