aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof.ml
AgeCommit message (Expand)Author
2020-11-16Deprecate `Grab Existential Variables` and `Existential` commandsMaxime Dénès
2020-09-01Unify the shelvesMaxime Dénès
2020-08-31Update update_global_env usageGaëtan Gilbert
2020-08-26Wrap future goals into a moduleMaxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-26Better encapsulation of future goalsMaxime Dénès
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
2020-06-26[declare] Remove mutual internals from Info.t structure.Emilio Jesus Gallego Arias
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
2020-01-30[exn] Don't reraise in exception printersEmilio Jesus Gallego Arias
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-07-11[proof] Minor cleanup in proof.mlEmilio Jesus Gallego Arias
2019-06-24[proof] Move initial_euctx to proof_globalEmilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2019-01-21At Qed, if shelved goals remain, emit a warning instead of an errorMaxime Dénès
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-11-22Merge PR #8967: Fix #8922 (uncaught pp_diff exception)Hugo Herbelin
2018-11-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
2018-11-14Get hyps and goal the same way Printer does; don't omit infoJim Fehrle
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-09-17Ensure_prev_proof returns a proof that has underlying differences fromJim Fehrle
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:08:56 +0000