aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.mli
AgeCommit message (Expand)Author
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-04-29Merging Context and Sign.ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-14Integrated obligations/eterm and program well-founded fixpoint building to to...msozeau
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-05-17Break circular dependency Proof_global -> Vernacexpr -> Proof_global.aspiwack
2011-05-13New option [Set Bullet Behavior] allows to select the behaviour of bullets.aspiwack
2011-04-29Some comments.aspiwack
2011-02-10Started to fix the declarative proof mode (C-zar).aspiwack
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-05Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proofpboutill
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack