aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.ml
Commit message (Expand)AuthorAge
...
* A "Grab Existential Variables" to transform the unresolved evars at the end o...Gravatar aspiwack2012-02-07
* In emacs mode, prints a list of the dependent existential variables introducedGravatar aspiwack2011-11-23
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...Gravatar aspiwack2011-09-12
* Fixes mini-bug: Qed would succeed even on focused proofs.Gravatar aspiwack2011-08-12
* A better procedure for checking presence of undefined evars.Gravatar aspiwack2011-05-13
* The modules in proofs now use the Errors module to explain their exceptions t...Gravatar aspiwack2011-05-13
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* Fix minor typo in error message (Closes: #2408)Gravatar glondu2010-10-25
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22