aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif ↵herbelin
d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Amélioration message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1108 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Évaluation forcée des objets mis dans les streamsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1107 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Autorisation de parenthèses autour des constructeurs dans le filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1098 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Bug dans les alias de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1095 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14On force l'évaluation du qualid_of_global qui peut échouer dans le débuggerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1094 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 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-06Modif rapide pour prise en compte eqTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1078 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06MAJ nom long de eqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1076 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06section_path etait en fait bonne dans ast et buggee dans printer.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1074 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-062ème bug de traduction des Pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1072 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Bug de traduction des Pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1071 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-06Notion de 'clause_pattern' pour désigner un ensemble d'occurrences dans le ↵herbelin
but et ses hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1065 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-29Prise en compte REQUIRE dans print_leafherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1036 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29ajoutfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1030 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Now AddRecPath and AddPath can be used with an As option to specify thesacerdot
Coq dir path. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1025 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath ↵herbelin
pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-10 15:04:47 +0000