aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2005-11-26coqide send a ack to tell drgeocaml it is receivednarboux
2005-11-25majcoq
2005-11-25*** empty log message ***barras
2005-11-25*** empty log message ***barras
2005-11-24majcoq
2005-11-23majcoq
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-22majcoq
2005-11-21majcoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 18:56:37 +0000