aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.ml
AgeCommit message (Expand)Author
2011-08-10Graceful error message for [Proof Mode] and [Set Default Proof Mode] when req...aspiwack
2011-07-11Stores bullet stack on locally at the level of focuses rather than globally i...aspiwack
2011-07-06Fixed bullets so that they would play well with { }.aspiwack
2011-05-17Break circular dependency Proof_global -> Vernacexpr -> Proof_global.aspiwack
2011-05-17Fixes bug in [maximal_unfocus] introduced in r14120.aspiwack
2011-05-13The modules in proofs now use the Errors module to explain their exceptions t...aspiwack
2011-05-13New option [Set Bullet Behavior] allows to select the behaviour of bullets.aspiwack
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-02-10Started to fix the declarative proof mode (C-zar).aspiwack
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack