aboutsummaryrefslogtreecommitdiff
path: root/proofs/pfedit.mli
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-06-24[proof] Remove last case of optional `?poly` arguments.Emilio Jesus Gallego Arias
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio 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-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-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
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-07-05refine: obey the use_unification_heuristics flagMatthieu Sozeau
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-11-29[proof] [api] Rename proof types in preparation for functionalization.Emilio Jesus Gallego Arias
2017-11-13[api] Insert miscellaneous API deprecation back to core.Emilio Jesus Gallego Arias
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-07[api] Remove 8.7 ML-deprecated functions.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27contracting the type of "Pfedit.solve_by_implicit_tactic"Matej Košík
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
2017-03-23Fast path for implicit tactic solving.Pierre-Marie Pédrot
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-28Fix bug #4723 and FIXME in API for solve_by_tacMatthieu Sozeau
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-09-08Making Proof_global terminator generic in external tactics.Pierre-Marie Pédrot
2016-08-25CLEANUP: Type alias "Context.section_context" was removedMatej Kosik
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-05-26Pfedit.get_current_context refinement (fix #4523)Matthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2015-11-28Univs: correctly register universe binders for lemmas.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-09-23Removing the generalization of the body of inductive schemes fromHugo Herbelin
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:43:22 +0000