aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2006-01-03Modification pour que l'ordre des éléments respecte l'ordre dans lequel ils...herbelin
2005-12-28Remplacement Pp.qs par Pptactic.qsnewherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-23bug de coqide sous windows (bad file descriptor)barras
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-02Types inductifs parametriquesmohring
2005-08-19pas besoin de List.length pour savoir si une liste est videletouzey
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
2005-05-26New environment variable COQREMOTEBROWSER to set the command used by Coqsacerdot
2005-05-19Déplacement de fonctionnalités unix et browser de ide vers libherbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-04-20Implementation of a new backtracking system, that allow to go backcoq
2005-02-04Bug synchronisation fonction connectherbelin
2005-02-04Ajout d'un processus de communication entre Coq et un outil externeherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-14Code redondant (cf Printer)herbelin
2004-12-24Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...herbelin
2004-11-12Changement dans les boxed values .gregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-10-12option -no-hash-consing pour supprimmer le hash-consingfilliatr
2004-09-06optimized the non-backtracking casebarras
2004-07-29Protection unlocherbelin
2004-07-29Bug join_locherbelin
2004-07-27Utilisation de la variable camlp4 OCAML_308 plutôt que d'en reconstruire un...herbelin
2004-07-17Backtrack sur l'utilisation de pa_macro car n'existait pas en 3.06herbelin
2004-07-16Mise en place mécanisme de compatibilité ocaml 3.08herbelin
2004-07-16Nouvelle en-têteherbelin
2004-05-08un argument booleen inutilisé dans expand_macrosletouzey
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts fix...barras
2004-02-16Erreur dépendance en Util lui-mêmeherbelin
2004-02-13Ajout array_map_left and coherbelin
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
2004-01-29Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...herbelin
2003-12-31*** empty log message ***barras
2003-11-26Export string_index_fromherbelin
2003-10-16Marge presqu'a 80, maximum indentation a 50 pour une meilleure lisibiliteherbelin
2003-10-13Ajout projections de tripletherbelin
2003-10-11reparation Undo suiteherbelin
2003-10-10Bug undoherbelin
2003-10-10Gestion en temps constant de la pile des Unfoherbelin
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-09-22Passage à la V8 par défautherbelin
2003-09-14Bug PR#324herbelin
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...herbelin
2003-09-10warning vers std_errherbelin
2003-08-14Positionnement precoce de l'option -v7herbelin
2003-08-11Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:47:48 +0000