aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.mli
Commit message (Expand)AuthorAge
* Forward-port fixes from 8.4 (15358, 15353, 15333).Gravatar msozeau2012-06-04
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Fixes bug #2654 (tactic instantiate failing to update existential variables).Gravatar aspiwack2012-01-06
* 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
* Factorize code of rewrite to make way for a new implementation using theGravatar msozeau2011-02-07
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* 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