aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Expand)AuthorAge
* Debugger vs tracer: Two different behaviors wrt printing: The debuggerGravatar herbelin2012-02-01
* Added new command "Set Parsing Explicit" for deactivating parsing (andGravatar herbelin2012-01-20
* Suspending declaration of undefined debug printers.Gravatar herbelin2011-12-18
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Revert "New evar_map printer ppevmfull which can typically be installed for"Gravatar herbelin2011-10-17
* New evar_map printer ppevmfull which can typically be installed forGravatar herbelin2011-10-17
* dev/base_include: display a nice message at the end of the loadGravatar letouzey2011-10-15
* debugging.txt: no more typing of #use "include" if using .ocamlinitGravatar letouzey2011-10-15
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Moving never-used comments from Zhints.v to dev/doc so as not toGravatar herbelin2011-10-01
* Polishing commits r14492, r14448 and r14407 (tactics propagateGravatar herbelin2011-09-25
* Fix unification: detect invalid evar instantiations due to scoping earlier.Gravatar msozeau2011-08-04
* Add printer dependency to Hashtbl_alt (used in Term)Gravatar puech2011-07-29
* Fixed a "feature" of "inversion" and "dependent rewrite" revealed byGravatar herbelin2011-07-18
* Finally, pr_goal seems to work for printing v8.2 style goal in debugger.Gravatar herbelin2011-07-16
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* A few comments and a dev file to summarize issues with unificationGravatar herbelin2011-06-13
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
* As many notation for for vectors as for List.Gravatar pboutill2011-05-03
* dev/base_include: no more mod_self_idGravatar letouzey2011-04-26
* - 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