aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-12-24Tentative de réparation du bug #1025: it seems like that a casted module sho...herbelin
2005-12-23majcoq
2005-12-23*** empty log message ***herbelin
2005-12-23Débranchement des parseurs de syntaxe v7herbelin
2005-12-23Simplifification de vernac_expr li l'abandon du traducteurherbelin
2005-12-23MAJ restructuration constrintern.mlherbelin
2005-12-23Vérification qu'un module est ouvert avant d'insérer une déclaration nommÃ...herbelin
2005-12-23Correction printer des Tactic Notationherbelin
2005-12-23Correction pr_module pour traducteurherbelin
2005-12-23Test printing of Tactic Notation which was broken until dec 2005herbelin
2005-12-22majcoq
2005-12-22Abandon tests syntaxe v7 (correction)herbelin
2005-12-22Contrepartie de la suppression des boites automatiques dans formatherbelin
2005-12-22option '-top dir' now works also in batch mode (2ème)herbelin
2005-12-22Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 15:23:58 +0000