aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.ml
Commit message (Expand)AuthorAge
* Introducing a notion of evar candidates to be used when an evar isGravatar herbelin2011-12-16
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...Gravatar aspiwack2011-09-12
* Porting Hendrik's 8.3 patch for proof tree visualization under proofGravatar herbelin2011-08-30
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* The modules in proofs now use the Errors module to explain their exceptions t...Gravatar aspiwack2011-05-13
* Factorize code of rewrite to make way for a new implementation using theGravatar msozeau2011-02-07
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefinedGravatar letouzey2010-12-13
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* 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
* Enlevé les trucs commités au mauvais endroitGravatar aspiwack2007-10-23
* Quelques structures de donnée plus les modules principaux (et Gravatar aspiwack2007-10-23