aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof.ml
AgeCommit message (Expand)Author
2018-03-08Add an invariant on future goals in Proof.run_tactic.Hugo Herbelin
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-29[proof] [api] Rename proof types in preparation for functionalization.Emilio Jesus Gallego Arias
2017-11-19[proof] Attempt to deprecate some V82 parts of the proof API.Emilio Jesus Gallego Arias
2017-11-13[api] Insert miscellaneous API deprecation back to core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-01-26Adding a printer for Proof.proof reflecting the focusing layout.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 01:21:01 +0000