aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.ml
Commit message (Expand)AuthorAge
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Forward-port fixes from 8.4 (15358, 15353, 15333).Gravatar msozeau2012-06-04
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Fixes bug #2654 (tactic instantiate failing to update existential variables).Gravatar aspiwack2012-01-06
* 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