aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-12-22option '-top dir' now works also in batch mode; it is even necessary to ensur...herbelin
2005-12-22Double bug de interp_modifiers anciennement caché par un troisième que les ...herbelin
2005-12-22Correction bugs commit précédentherbelin
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2005-12-21Abandon tests syntaxe v7; ajouts tests modulesherbelin
2005-12-21majcoq
2005-12-21MAJ syntaxe v7 avant activation en syntaxe v8herbelin
2005-12-21Activation du test de Refine en v7 pour mémoire avant passage à la v8herbelin
2005-12-21Anciennement déplacé dans 'output'herbelin
2005-12-21cf ltac4.vherbelin
2005-12-21MAJherbelin
2005-12-21Divers; restructuration des points d'entrée de Constrinternherbelin
2005-12-21Prise en compte de l'information que certaines tactiques attendent un type (u...herbelin
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
2005-12-21Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...herbelin
2005-12-21Uniformisation: extension de la suppression d'un casts dans collapse_app à l...herbelin
2005-12-20majcoq
2005-12-20Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...herbelin
2005-12-19majcoq
2005-12-19Suppression de la mise en boite automatique si format utilisateurherbelin
2005-12-18majcoq
2005-12-18L'option -no-vm laisse la place à une option -vmherbelin
2005-12-17majcoq
2005-12-17majcoq
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-16majcoq
2005-12-16amelioration de l'extraction haskell: affichage du type des fonctions, et sup...letouzey
2005-12-16multiples ameliorations de l'extraction scheme:letouzey
2005-12-15majcoq
2005-12-15correction d'un bug dans le make installnarboux
2005-12-14majcoq
2005-12-13changing the name of drgeocaml into GeoProofnarboux
2005-12-08More exception handling in functional scheme.coq
2005-12-06j'avais oublie ces deux fichiers.gregoire
2005-12-05correction bug 881.gregoire
2005-12-05changement d'egalite pour le named_context_valgregoire
2005-12-02Changement des named_contextgregoire
2005-12-01amelioration de la generation des unsafeCoerceletouzey
2005-11-30changement parametres inductifs dans les theoriesmohring
2005-11-30evite certaines eta-expansions cavalieresletouzey
2005-11-29correctif pour que type t = M.t contienne bien son M.letouzey
2005-11-29majcoq
2005-11-28majcoq
2005-11-28majcoq
2005-11-28parametres inductifsmohring
2005-11-27majcoq
2005-11-26majcoq
2005-11-26Fonctionnalisation du cache 'compunit' pour réparer correctement le bug #103...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 17:00:37 +0000