aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof.mli
AgeCommit message (Expand)Author
2020-11-26[proofs] Support per-definition typing-flags in interactive proofs.Emilio Jesus Gallego Arias
2020-09-01Unify the shelvesMaxime Dénès
2020-08-31Update update_global_env usageGaëtan Gilbert
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
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
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-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
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-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-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
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-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-26[api] Remove aliases of `Evar.t`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-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-01-26Adding a printer for Proof.proof reflecting the focusing layout.Hugo Herbelin
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-02-23Fix some typos in comments.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-01Add [Info] command.Arnaud Spiwack
2014-10-22Remove unused functions for side effects.Arnaud Spiwack
2014-10-01Factored out IDE goal structure.Carst Tankink
2014-07-31Making the error message about bullets more precise.Pierre Courtieu
2014-07-23Proof_global.start_dependent_proof: properly threads the sigma through the te...Arnaud Spiwack
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu 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-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:36:36 +0000