aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Expand)AuthorAge
* - Remove create_evar_defsGravatar msozeau2011-04-13
* Fix dev/base_include after change of constant_bodyGravatar letouzey2011-04-06
* Adapt printers.mllib after my last commitGravatar letouzey2011-03-16
* Annotations at functor applications:Gravatar letouzey2011-02-11
* Update changelogsGravatar glondu2011-02-11
* Factorize code of rewrite to make way for a new implementation using theGravatar msozeau2011-02-07
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Prepare change of nomenclature rawconstr -> glob_constrGravatar glondu2010-12-23
* Print universes in debugging printersGravatar glondu2010-11-08
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* Remove Explain* vernacsGravatar glondu2010-10-06
* Install a printer for fconstr (ppconstr was installed twice)Gravatar glondu2010-10-04
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...Gravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Updated COPYRIGHT file and header. Improved and fixed header updater.Gravatar herbelin2010-07-24
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Turned off Mac dynlink hack for 10.6.3+ on x86_64Gravatar thutchin2010-07-05
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Names: remove obsolete mod_self_idGravatar letouzey2010-06-23
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Quick fix for having clenv debug printer working in trunk.Gravatar herbelin2010-06-18
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
* Fixed a bug in pretty-printing "induction" and "destruct" due to aGravatar herbelin2010-06-13
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Added debugging printer for the idmap used at evar definition time forGravatar herbelin2010-06-12
* Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.Gravatar herbelin2010-06-09
* Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)Gravatar glondu2010-06-07
* Updated performance analysis fileGravatar herbelin2010-06-06
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* ocamldoc related fixesGravatar pboutill2010-05-03
* "make source-doc" builds documentation of mli in html and pdf atGravatar pboutill2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Removing redundant internal variants of apply tactic and simplification of ML...Gravatar herbelin2010-04-14
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...Gravatar letouzey2010-03-04
* Makefile: make devdocclean was not removing *.dep.ps, btw let's remove *.dep....Gravatar letouzey2010-03-04
* Remove bashismsGravatar glondu2010-01-28
* Added module sharing support for typeclasses and hints (pri_auto_tactic).Gravatar soubiran2010-01-12
* * Segmenttree: New. A very simple implementation of segment trees.Gravatar regisgia2010-01-08
* Few misc. updates.Gravatar herbelin2010-01-04
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* * Rewrite [classify_unicode] using standard unicode tables.Gravatar regisgia2009-12-20
* Addition of mergesort + cleaning of the Sorting libraryGravatar herbelin2009-12-13