aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.ml
AgeCommit message (Expand)Author
2013-12-04Allow proofs to start with dependent goals.Arnaud Spiwack
2013-11-04Allowing proofs starting with a non-empty evarmap.ppedrot
2013-11-02Adds a tactic give_up.aspiwack
2013-11-02Adds a shelve tactic.aspiwack
2013-11-02New option Default Goal Selector.aspiwack
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-31Future: better doc + restore ~pure optimizationgareuselesinge
2013-10-18proof modes: use ephemerons to represent them in proof stategareuselesinge
2013-10-18declaration_hooks use Ephemerongareuselesinge
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-30safe Conv_oracle state for type checkinggareuselesinge
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
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-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (proof)ppedrot
2012-10-06still some more dead code removalletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-20Arranged for the desirable behaviour that bullets do not see beyond braces.aspiwack
2012-03-14Integrated obligations/eterm and program well-founded fixpoint building to to...msozeau
2012-03-02Noise for nothingpboutill
2012-01-06Forbids (as it has always been the behaviour) to have two different openaspiwack
2011-12-12Proof using ...gareuselesinge
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-14Bug 2636 - Move string_of_ppcmds to Pppboutill
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:45:37 +0000