aboutsummaryrefslogtreecommitdiff
path: root/proofs/pfedit.ml
AgeCommit message (Expand)Author
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-07-11[proof] Minor cleanup in proof.mlEmilio Jesus Gallego Arias
2019-06-24[proof] Remove last case of optional `?poly` arguments.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] More uniformity in proof start labels.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
2019-06-24[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-04-24Fix proof bullet error helper (nosuchgoal)Gaëtan Gilbert
2019-04-24[proof] Fix proof bullet error helper which was implemented as a hookEmilio Jesus Gallego Arias
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
2019-03-27[proof_global] Removal of imperative state.Emilio Jesus Gallego Arias
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2018-12-19Merge PR #9139: [engine] Allow debug printers to access the environment.Pierre-Marie Pédrot
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-12-13[engine] Allow debug printers to access the environment.Emilio Jesus Gallego Arias
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-19[pfedit] Remove `start_proof` stub from `Pfedit`Emilio Jesus Gallego Arias
2018-11-17[pfedit] Remove cook_proof stub.Emilio Jesus Gallego Arias
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-09-20Current diff code only compares the first current goal of the old and newJim Fehrle
2018-09-06[pfedit] Fix master build due to merge conflictEmilio Jesus Gallego Arias
2018-08-28Fix #7795: UGraph.AlreadyDeclared with ProgramGaëtan Gilbert
2018-06-04[econstr] Remove some Unsafe.to_constr use.Emilio Jesus Gallego Arias
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-11-19[proof] Attempt to deprecate some V82 parts of the proof API.Emilio Jesus Gallego Arias
2017-11-07[api] Remove 8.7 ML-deprecated functions.Emilio Jesus Gallego Arias
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-07-26Statically ensuring that inlined entries out of the kernel have no effects.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:34:19 +0000