aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Added 'clear - id' to clear all hypotheses except the ones dependent in the s...Gravatar herbelin2005-03-07
* Added 'clear - id' to clear all hypotheses except the ones dependent in the s...Gravatar herbelin2005-03-07
* Keep ClosedSection marker for resetGravatar herbelin2005-02-20
* Renaming Print Canonical Structure into Print Canonical ProjectionsGravatar herbelin2005-02-18
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* Bug affichage entiers négatifsGravatar herbelin2005-02-17
* Nouvelle mouture Print Canonical StructuresGravatar herbelin2005-02-12
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
* Parseur pour la DTD XML de constr et un peu plus pour les arguments de tactiquesGravatar herbelin2005-02-04
* Ajout constructeur External pour appel outil externe à CoqGravatar herbelin2005-02-04
* Clarification des niveaux pr_constr et pr_lconstr en v8 dans pr_prim_rule (cu...Gravatar herbelin2005-02-03
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Pour cible make docGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Ajout de la syntaxe du reset label: "BackTo n".Gravatar coq2005-01-14
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Amélioration message LocateGravatar herbelin2005-01-13
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
* HUGE COMMITGravatar sacerdot2005-01-03
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...Gravatar herbelin2004-12-29
* Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...Gravatar herbelin2004-12-25
* TypoGravatar herbelin2004-12-24
* Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...Gravatar herbelin2004-12-24
* Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...Gravatar herbelin2004-12-22
* Restauration type casted_open_constr pour tactique refine car l'unification n...Gravatar herbelin2004-12-09
* Amélioration message localisation constructions et modulesGravatar herbelin2004-12-09
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
* The type Pattern.constr_label was isomorphic to Libnames.global_reference.Gravatar sacerdot2004-12-07
* Uniformisation du nom d'entrée openconstr en le nom du type open_constrGravatar herbelin2004-12-06
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...Gravatar herbelin2004-12-06
* Indépendance vis à vis de Symbols (suite)Gravatar herbelin2004-11-27
* Bug commit 1.71Gravatar herbelin2004-11-22
* Correction bug Notation: il faut re-déclarer les règles de parsing des nota...Gravatar herbelin2004-11-22
* compatibility with POWERPCGravatar gregoire2004-11-22
* 'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marcheGravatar herbelin2004-11-20
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* Ajout 'Locate Module'Gravatar herbelin2004-11-17
* Déclaration de '..' comme mot-clé (résoud bug #856)Gravatar herbelin2004-11-17
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Correction bug #868Gravatar herbelin2004-11-10
* Univ.pr_univ ==> Univ.pr_uniGravatar sacerdot2004-11-04
* Affichage des universGravatar herbelin2004-11-04
* Bug mauvais nom d'entrée binder_constr quand récursion gaucheGravatar herbelin2004-10-27
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Desactivation de la construction 'lazy match' en attendant une autre solutionGravatar herbelin2004-10-12
* Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...Gravatar herbelin2004-10-12