aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2001-01-31Ajout option Set/Unset/Test Printing Coercionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1298 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-30backtrack sur le lexeur de la V6filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1289 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27Simplification Impargsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1284 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27Factorisation du '.' finalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1281 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27Ré-introduction des implicites à la volée dans la définition des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1279 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Prise en compte des noms longs dans les Hints et les Coercionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1272 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Ajout de constantes locales dans les Recordsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1266 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Prise en compte de constructeurs qualifiés dans les patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1261 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Nouveau module pour centraliser les chemins des constantes globales ↵herbelin
utilisées dans le code de Coq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1260 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Ajout d'un parseur d'entiers sous forme de patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1259 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Autour des quotations avec Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1258 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Réparation bug extensibilité de Constr.patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1257 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-09Meta Definition + Tactic Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1240 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1236 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-26Pattern sera mieux dans Pretyping; relâchement head_pattern_boundherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1219 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25bug head_pattern_boundherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1213 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Token n'est plus un keywordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1209 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Effet réorganisation Classopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1202 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22*** empty log message ***mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1197 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-21Qualification des inductifs dans Print indherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1181 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20espacementsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1177 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Suppression warning variable de filtrage en majusculeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1175 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-19Amélioration affichage Print ALlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1153 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-18Suppression de l'affichage des instances des ?nherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1144 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1133 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées ↵herbelin
'Set Implicit Arguments' and co git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1122 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-28 21:16:20 +0000