aboutsummaryrefslogtreecommitdiff
path: root/proofs/pfedit.ml
AgeCommit message (Expand)Author
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-11-02Doc: solve the bad interaction between Declare Implicit Tactic and refine.aspiwack
2013-11-02Adds a new goal selector "all:".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-18declaration_hooks use Ephemerongareuselesinge
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-08get rid of closures in global/proof stategareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-06-06Fixing bug #3030.ppedrot
2013-05-12Use the Hook module here and there.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-04-29Merging Context and Sign.ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (proof)ppedrot
2012-10-22Fix bug #2892letouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-01Cancel the start of a proof if its init_tac fails (fix #2799)letouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-05-29Pfedit: two superfluous openletouzey
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-21Pfedit: avoid Undoing too muchletouzey
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-05-13The modules in proofs now use the Errors module to explain their exceptions t...aspiwack
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-08Applying Tom Prince's patch for build_constant_by_tactic not able toherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 07:04:57 +0000