aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2005-12-21Divers; restructuration des points d'entrée de Constrinternherbelin
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
2005-12-20Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...herbelin
2005-12-19Suppression de la mise en boite automatique si format utilisateurherbelin
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...herbelin
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...herbelin
2005-12-17Orthographe de 'instantiate'herbelin
2005-12-02Changement des named_contextgregoire
2005-11-23bug de coqide sous windows (bad file descriptor)barras
2005-11-23bug #909: Top n'est cree que si le contexte est videbarras
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-08- debugging og "Show Intros": no line breaking + fresh idscoq
2005-11-04Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09herbelin
2005-11-02Types inductifs parametriquesmohring
2005-05-26No parentheses around f in 'f \subst{...}'herbelin
2005-05-26Utilisation du module Buffer; encodage plus rigoureux des symboles en uriherbelin
2005-05-26Patch to avoid Whelp bug removed.sacerdot
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
2005-05-20Interface vers outil de recherche Whelpherbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-05-15Globalisation des Tactic Notationherbelin
2005-04-20Implementation of a new backtracking system, that allow to go backcoq
2005-03-11Ajout récursif du répertoire COQLIB/user-contrib au chemin de chargementherbelin
2005-03-01Code mortherbelin
2005-02-20Keep ClosedSection marker for resetherbelin
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2005-02-06Nettoyage et documentation de Libraryherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-14Ajout de la syntaxe du reset label: "BackTo n".coq
2005-01-14Affichage numéro de l'état de la commande courante pour mode emacsherbelin
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
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...herbelin
2004-12-30Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ...herbelin
2004-12-09Amélioration message localisation constructions et modulesherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 04:53:37 +0000