aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2004-12-06Bug (cf #892)herbelin
2004-12-03Amélioration message d'erreur v8herbelin
2004-11-29Complétion commit précédentherbelin
2004-11-26Réduire pour trouver l'arité d'une classeherbelin
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-19Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREherbelin
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
2004-11-17Ajout 'Locate Module'herbelin
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-11-12*** empty log message ***gregoire
2004-11-12Changement dans les boxed values .gregoire
2004-11-08Prise en compte des notations récursives dans l'option 'format'herbelin
2004-10-27Non affichage des notations réduites à une variableherbelin
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-10-17Semble raisonnable de distinguer les noms aussi dans cant_applyherbelin
2004-10-12option -no-hash-consing pour supprimmer le hash-consingfilliatr
2004-10-11Suppression IsConjecture redondant avec Conjecturalherbelin
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-03deplacement de clenv vers pretypingbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-09-03Bug List.hd vs list_lastherbelin
2004-09-03MAJ options coqtop et coqcherbelin
2004-08-23Pas de notation v7 si purement en v8herbelin
2004-08-23Correction bug #830 : les noms des implicites temporaires étaient inconnus a...herbelin
2004-08-06Amélioration message d'erreur objet de récursion de type non inductifherbelin
2004-07-23"Print Setoids" command added.sacerdot
2004-07-17Backtrack sur l'utilisation de pa_macro car n'existait pas en 3.06herbelin
2004-07-16Abstraction vis à vis du type loc pour compatibilité ocaml 3.08herbelin
2004-07-16Branchement sur pa_macro, pa_ifdef devenant obsolete en 3.08herbelin
2004-07-16Nouvelle en-têteherbelin
2004-07-13bug #780: compilation of several units in the same coqtop processbarras
2004-07-13bug #790: better error_not_cleanbarras
2004-06-30updated printing of evar context (may loop ?)corbinea
2004-06-28Correction bug #776herbelin
2004-06-25correspondance des records et noms de champs de records entre un module et sa...letouzey
2004-06-02Recherche de la source à partir de la gauche pour gérer des cas comme 'Coer...herbelin
2004-05-26Affichage de la date de checkout même si pas dans le répertoire de compilationherbelin
2004-05-25Correction bug 'Time Load foo'herbelin
2004-05-14test de conversion laissait echapper exception NotConvertiblebarras
2004-04-17pb facto des Fixpoint + erreur avec -dump-glob et Loadbarras
2004-03-31Export de l'information si un inductive est un record ou non (pour xml)herbelin
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations uti...herbelin
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations uti...herbelin
2004-03-28Nom qualifié pour option -topherbelin
2004-03-28Ajout option -top pour changer le nom 'Top' du toplevelherbelin
2004-03-27Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...herbelin
2004-03-26Ajout entree pour exporter les debuts et fins de compilation en mode -xmlherbelin
2004-03-17Amelioration affichage des notationsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:40:53 +0000