aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2004-12-07* added subst_evaluable_referencesacerdot
2004-12-07The type Pattern.constr_label was isomorphic to Libnames.global_reference.sacerdot
2004-12-06Uniformisation du nom d'entrée openconstr en le nom du type open_constrherbelin
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...herbelin
2004-11-27Indépendance vis à vis de Symbols (suite)herbelin
2004-11-22Bug commit 1.71herbelin
2004-11-22Correction bug Notation: il faut re-déclarer les règles de parsing des nota...herbelin
2004-11-22compatibility with POWERPCgregoire
2004-11-20'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marcheherbelin
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
2004-11-17Ajout 'Locate Module'herbelin
2004-11-17Déclaration de '..' comme mot-clé (résoud bug #856)herbelin
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-11-12Changement dans les boxed values .gregoire
2004-11-10Correction bug #868herbelin
2004-11-04Univ.pr_univ ==> Univ.pr_unisacerdot
2004-11-04Affichage des universherbelin
2004-10-27Bug mauvais nom d'entrée binder_constr quand récursion gaucheherbelin
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-10-12Desactivation de la construction 'lazy match' en attendant une autre solutionherbelin
2004-10-12Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...herbelin
2004-10-12Réinstallation des lieurs avant l'énoncé de Theorem/Lemma (non documenté ...herbelin
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...herbelin
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
2004-09-08Meilleur anglais (cf #841)herbelin
2004-09-03deplacement de clenv vers pretypingbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-08-26Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...herbelin
2004-08-23Précisions message d'erreurherbelin
2004-07-29Distinction location ocaml 3.08 ou pas (suite)herbelin
2004-07-29Distinction location ocaml 3.08 ou pasherbelin
2004-07-28Bug tactique fixherbelin
2004-07-23"Print Setoids" command added.sacerdot
2004-07-20Abstraction vis à vis de dummy_locherbelin
2004-07-16Abstraction vis à vis du type loc pour compatibilité ocaml 3.08herbelin
2004-07-16Suppression quotifyherbelin
2004-07-16Nouvelle en-têteherbelin
2004-07-16Branchement sur Util.loc et abstraction vis a vis de dummy_locherbelin
2004-07-16Abstraction vis a vis de dummy_locherbelin
2004-07-13bugs #667 and #783 (mimick_evar and loc_table on large files)barras
2004-06-29moved instantiate binding to extratacticscorbinea
2004-06-29efficacite du lexeurfilliatr
2004-06-28more evar stuffcorbinea
2004-06-17Nouvelle syntaxe à la ML pour donner le type ML des extensions d'argumentsherbelin
2004-06-03Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)herbelin
2004-06-02Affichage de l'opacité dans Print et Aboutherbelin
2004-05-27Bug affichage ClearBodyherbelin
2004-05-14Bug syntaxe AddPathherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 17:55:46 +0000