aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]bherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2170 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 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-24Suppression de Logic_Type.sigT, redondant avec Specif.sigTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2139 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵herbelin
sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-15Nouvelle correction du bug confusion entre implicites de locaux et de globauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2115 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵herbelin
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 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-11Bug collision entre les implicites d'un global et les variables locales de ↵herbelin
même nom court git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2108 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-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-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-24Marre des unrecognized objectsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2055 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Réparation des options Set Printing and coherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2052 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Mise en place globalisation optionnelle pour Infix/Distfixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2046 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Amélioration affichage de print_leaf_entryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2040 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Rajout 'Set Printing Depth'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2039 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-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵herbelin
des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et ↵herbelin
le «load» des Remark/Fact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1998 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14Search prenait en compte le contenu des sections alors que celui-ci n'existe ↵herbelin
plus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1972 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1970 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-09-13Prise en compte qualid dans Hint Unfoldherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1961 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵herbelin
éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1946 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1938 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-06Rétablissement de Print Sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1926 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-13bug incompatibilitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1895 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Pour contourner un bug de camlp4 3.02herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1894 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-06Nouvelle entrée ident_or_numargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1881 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-19Changements dans le traitement des qualid'sdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1859 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-19modifs de preuves (plus simples)mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1858 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-13reparation regles pour parsing Coercion Localmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1849 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-04ajout Show Intro(s)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1825 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-07-02Ajout glob_eq{,T}herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1818 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-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
n'etaient pas affiches correctement lors du Save si on les avait donne en argument de tactique. Avec Bruno, nous avons simplifie l'ast en remplacant les MLCASE NOREC et autres CASE NOREC par des choses plus simples. Il y a maintenant un noeud LET, un IF, un CASE et un MATCH qui sont a peu pres semblables mais qui permettent de se souvenir quoi afficher. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1781 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-05-29Retablissement de minicoqcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1773 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 15:22:52 +0000