aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof.ml
AgeCommit message (Expand)Author
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-11Fix bug #5123: mark all shelved evars unresolvableMatthieu Sozeau
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-20Extruding the code for the Existential command from Proofview.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-09-20Proof: suggest Admitted->Qed only if the proof is really complete (#4349)Enrico Tassi
2015-05-29STM/Univ: save initial univs (the ones in the statement) in Proof.proofEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-12-12Make sure the goals on the shelve are identified as goal and unresolvable for...Arnaud Spiwack
2014-11-28Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.Arnaud Spiwack
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-01Add [Info] command.Arnaud Spiwack
2014-11-01An API for info traces.Arnaud Spiwack
2014-10-23Evd.future_goals: forgot to revert the list in two places.Arnaud Spiwack
2014-10-22Proofview: move [list_goto] to the [CList] module.Arnaud Spiwack
2014-10-22Proofview: remove a redundant primitive.Arnaud Spiwack
2014-10-22Proofview: move more functions to the Unsafe module.Arnaud Spiwack
2014-10-22Remove unused functions for side effects.Arnaud Spiwack
2014-10-16Refactoring proofview: make the definition of the logic monad polymorphic.Arnaud Spiwack
2014-10-16Put evars remaining after a tactic on the shelf.Arnaud Spiwack
2014-10-16Goal: remove [advance] from the API.Arnaud Spiwack
2014-10-01Factored out IDE goal structure.Carst Tankink
2014-07-25Small reorganisation in proof.ml.Arnaud Spiwack
2014-07-25Fail gracefully when focusing on non-existing goals with user commands.Arnaud Spiwack
2014-07-23Proof_global.start_dependent_proof: properly threads the sigma through the te...Arnaud Spiwack
2014-04-07Transfering the initial goals from the proofview to the proof object.Pierre-Marie Pédrot
2013-12-11Fixing backtrace registering of various tactic-related try-with blocks.Pierre-Marie Pédrot
2013-12-04Allow proofs to start with dependent goals.Arnaud Spiwack
2013-11-04Allowing proofs starting with a non-empty evarmap.ppedrot
2013-11-02Update comments.aspiwack
2013-11-02Adds a tactic give_up.aspiwack
2013-11-02Adds a shelve tactic.aspiwack
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
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-04-29Merging Context and Sign.ppedrot
2013-03-16another Errors.push in a exception reraiseletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2012-11-25Monomorphization (proof)ppedrot
2012-10-02Remove the unused "intel" field in Proof.proof_stateletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-08-08Updating headers.herbelin
2012-07-04Change how the number of open goals is printed.aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:38:59 +0000