aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2000-11-28Ajout des Fix et CoFix dans les patternsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1004 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-27Bug affichage inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@996 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27uniformisation messages d'erreurfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@993 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Prise en compte des implicites de locaux à l'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@983 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Affichage des définitions localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@974 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Restruration autour de qualidargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@962 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-26Prise en compte noms longs dans divers fonctions de Printherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@959 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Réorganisation autour de globalize_constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@952 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@951 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Ajout d'un ↵herbelin
.:/opt/kde/bin:/home/herbelin/bin:/bin:/sbin:/usr/bin:/usr/etc:/usr/sbin:/usr/local/bin:/usr/X11/bin:/usr/games: comme macro des quotations d'ast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@950 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 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-24SearchPattern et SearchRewritefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@943 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Ajout d'une syntaxe pour Reals.mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@937 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Search réparéfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@932 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@929 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@924 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-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵herbelin
'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22deplacement poly_args; iterateurs sur les segmentsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Begin-End Silent deviennent Set?Unset Silentmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@899 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Prise en compte des implicites dans les regles de grammairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@895 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20La variable argument d'un non-terminal dans Grammar est maintenant un Var ( ↵herbelin
plus un Id ) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@892 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte des noms qualifiés dans certaines commandesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@891 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Nouveau lexeme METAIDENT pour les $idherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@890 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout diverses entrées pour les noms qualifiésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@889 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte des noms qualifiés dans certaines commandesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@884 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Acceptation des noms qualifiés; utilisation de global_reference dans ↵herbelin
pattern; prise en compte des noms qualifiés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@881 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-20Acceptation des noms qualifiés; nouveau lexeme METAIDENT pour les $idherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@879 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20"Distinction entre . suivi d'un blanc et . suivi d'un ident (pour les noms ↵herbelin
qualifiés; nouveau lexeme METAIDENT pour les \$id' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@878 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@876 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@873 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte constructeur QUALID pour noms qualifiésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@865 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte des noms qualifiés dans certaines commandes; nouveau lexeme ↵herbelin
METAIDENT pour les $id; nouvelle entrée pour les noms qualifiés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@864 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout pr_global_reference et is_visibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@856 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09Amélioration message d'erreur arg explicité au lieu d'arg normalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@838 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08nouveau load pathfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08out_variable (Liboject.obj -> ...) distibgue de get_variablefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@821 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@817 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@814 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ↵herbelin
DischargeAt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des ↵filliatr
constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-05Nouveau mode de compilation de .ml4herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@805 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-05Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier ↵herbelin
devenu tros gros pour la compilation en PowerPC git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@800 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-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-31- simplification Makefile (compilation des fichiers .ml'; pas encore parfaitfilliatr
car on passe par les fichiers .ml) - Require Export enfin rétabli avec la bonne sémantique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@792 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-30 01:17:32 +0000