aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2009-02-09memoized is_ground_envbarras
2009-01-27- Fixed various Overfull in documentation.herbelin
2009-01-23Petit nettoyage faisant suite au commit #11847 .aspiwack
2009-01-22Util.split_at : for quadratic to linear complexityletouzey
2009-01-19Experimental file commited by mistake, sorry.herbelin
2009-01-18Backporting from v8.2 to trunk:herbelin
2009-01-17DISCLAIMERpuech
2009-01-08Remove trailing newlines in outputs of X -whereglondu
2009-01-02Made the debugger work again:herbelin
2008-12-30- Fixed bugs and compatibilities issues in herbelin
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
2008-12-15Add some unicode symbols from japanese CJC (request by Y. Regis-Gianas)letouzey
2008-11-24eventually fixing r11612barras
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
2008-11-22- Fixed minor bug #1994 in the tactic chapter of the manual [doc]herbelin
2008-11-21fixed problem with r11612barras
2008-11-05Better extraction renaming phase (fix #1914 plus other non-reported bugs)letouzey
2008-11-04Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)herbelin
2008-10-27- Fixed many "Theorem with" bugs.herbelin
2008-10-23Open notation for declaring record instances.msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-09-02avoid small overflowsbarras
2008-08-04Évolutions diverses et variées.herbelin
2008-07-27Now, -browser option is effective (and compiles)glondu
2008-07-27(Partially) Revert previous commit because of FTBFSglondu
2008-07-27Add -browser option to configure scriptglondu
2008-07-24Suite commit 11236notin
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...notin
2008-07-16Quelques modifications autour du filtrage Ltac:herbelin
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-06-30Fichiers oubliés lors du 11188 :-(herbelin
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-24Suppression de l'option -dump-glob et ajout d'une option -no-globnotin
2008-06-09- Correction de la version simplifiée (filtrage sur deux sigherbelin
2008-06-09- Documentation de admit et Print Assumptions.herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-06-06Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematicalherbelin
2008-05-30- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"herbelin
2008-05-28debug : case where length of s is < 2...jnarboux
2008-05-26debug subst_command_placeholder : replace %s and not only %jnarboux
2008-05-24Ajout de la possibilité d'utiliser fix/cofix dans les notations.herbelin
2008-05-15Various fixes:msozeau
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-10Correction bug #1842 + correction bug initialisation introduit dansherbelin
2008-05-10- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desherbelin
2008-05-08Suite 10904 (fichiers oubliés)herbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-16Added a function that escapes XML characters in ppcmds.cek