aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof.mli
Commit message (Expand)AuthorAge
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Added a command "Unfocused" which returns an error when the proof isGravatar aspiwack2012-03-30
* Arranged for the desirable behaviour that bullets do not see beyond braces.Gravatar aspiwack2012-03-20
* Removed a superfluous function in proof.mli. Preparing for incomingGravatar aspiwack2012-03-01
* A "Grab Existential Variables" to transform the unresolved evars at the end o...Gravatar aspiwack2012-02-07
* Typo in comments.Gravatar aspiwack2012-02-07
* Proof using ...Gravatar gareuselesinge2011-12-12
* 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
* Fixed bullets so that they would play well with { }.Gravatar aspiwack2011-07-06
* Fixed a bug causing inconsistent states during proof editting.Gravatar aspiwack2011-04-29
* Some comments.Gravatar aspiwack2011-04-29
* Started to fix the declarative proof mode (C-zar).Gravatar aspiwack2011-02-10
* 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