aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2011-02-07Factorize code of rewrite to make way for a new implementation using themsozeau
2010-12-24Remove obsolete script univdot, update dev doc about universesglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-23Prepare change of nomenclature rawconstr -> glob_constrglondu
2010-11-08Print universes in debugging printersglondu
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-10-06Remove Explain* vernacsglondu
2010-10-04Install a printer for fconstr (ppconstr was installed twice)glondu
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-24dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...letouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-24Updated COPYRIGHT file and header. Improved and fixed header updater.herbelin
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
2010-07-05Turned off Mac dynlink hack for 10.6.3+ on x86_64thutchin
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-23Names: remove obsolete mod_self_idletouzey
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-18Quick fix for having clenv debug printer working in trunk.herbelin
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
2010-06-13Fixed a bug in pretty-printing "induction" and "destruct" due to aherbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-12Added debugging printer for the idmap used at evar definition time forherbelin
2010-06-09Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.herbelin
2010-06-07Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)glondu
2010-06-06Updated performance analysis fileherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-05-03ocamldoc related fixespboutill
2010-04-29"make source-doc" builds documentation of mli in html and pdf atpboutill
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-14Removing redundant internal variants of apply tactic and simplification of ML...herbelin
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ...herbelin
2010-03-04Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...letouzey
2010-03-04Makefile: make devdocclean was not removing *.dep.ps, btw let's remove *.dep....letouzey
2010-01-28Remove bashismsglondu
2010-01-12Added module sharing support for typeclasses and hints (pri_auto_tactic).soubiran
2010-01-08* Segmenttree: New. A very simple implementation of segment trees.regisgia
2010-01-04Few misc. updates.herbelin
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-12-20* Rewrite [classify_unicode] using standard unicode tables.regisgia
2009-12-13Addition of mergesort + cleaning of the Sorting libraryherbelin
2009-12-02Remove interface pluginglondu
2009-11-13Remove useless ppevd (which is identical to ppevm)glondu
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-11-11Fixed bug #2168 (closing a section may have as side-effect the erasureherbelin
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:54:46 +0000