aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Ajout récursif du répertoire COQLIB/user-contrib au chemin de chargementGravatar herbelin2005-03-11
* Code mortGravatar herbelin2005-03-01
* Keep ClosedSection marker for resetGravatar herbelin2005-02-20
* Renaming Print Canonical Structure into Print Canonical ProjectionsGravatar herbelin2005-02-18
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Compatibilité ocamlweb pour cible 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
* Affichage numéro de l'état de la commande courante pour mode emacsGravatar herbelin2005-01-14
* - 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
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ...Gravatar herbelin2004-12-30
* Amélioration message localisation constructions et modulesGravatar herbelin2004-12-09
* Bug (cf #892)Gravatar herbelin2004-12-06
* Amélioration message d'erreur v8Gravatar herbelin2004-12-03
* Complétion commit précédentGravatar herbelin2004-11-29
* Réduire pour trouver l'arité d'une classeGravatar herbelin2004-11-26
* 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
* Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREGravatar herbelin2004-11-19
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* Ajout 'Locate Module'Gravatar herbelin2004-11-17
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* *** empty log message ***Gravatar gregoire2004-11-12
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Prise en compte des notations récursives dans l'option 'format'Gravatar herbelin2004-11-08
* Non affichage des notations réduites à une variableGravatar herbelin2004-10-27
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Semble raisonnable de distinguer les noms aussi dans cant_applyGravatar herbelin2004-10-17
* option -no-hash-consing pour supprimmer le hash-consingGravatar filliatr2004-10-12
* Suppression IsConjecture redondant avec ConjecturalGravatar herbelin2004-10-11
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* deplacement de clenv vers pretypingGravatar barras2004-09-03
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Bug List.hd vs list_lastGravatar herbelin2004-09-03
* MAJ options coqtop et coqcGravatar herbelin2004-09-03
* Pas de notation v7 si purement en v8Gravatar herbelin2004-08-23
* Correction bug #830 : les noms des implicites temporaires étaient inconnus a...Gravatar herbelin2004-08-23
* Amélioration message d'erreur objet de récursion de type non inductifGravatar herbelin2004-08-06
* "Print Setoids" command added.Gravatar sacerdot2004-07-23
* Backtrack sur l'utilisation de pa_macro car n'existait pas en 3.06Gravatar herbelin2004-07-17