aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-02-17Bug affichage entiers négatifsherbelin
2005-02-12Nouvelle mouture Print Canonical Structuresherbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2005-02-04Parseur pour la DTD XML de constr et un peu plus pour les arguments de tactiquesherbelin
2005-02-04Ajout constructeur External pour appel outil externe à Coqherbelin
2005-02-03Clarification des niveaux pr_constr et pr_lconstr en v8 dans pr_prim_rule (cu...herbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-21Pour cible make docherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-14Ajout de la syntaxe du reset label: "BackTo n".coq
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
2005-01-13Amélioration message Locateherbelin
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
2005-01-06- Module/Declare Module syntax made more uniform:sacerdot
2005-01-03HUGE COMMITsacerdot
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin
2004-12-29ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...herbelin
2004-12-25Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...herbelin
2004-12-24Typoherbelin
2004-12-24Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...herbelin
2004-12-22Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...herbelin
2004-12-09Restauration type casted_open_constr pour tactique refine car l'unification n...herbelin
2004-12-09Amélioration message localisation constructions et modulesherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 23:36:12 +0000