aboutsummaryrefslogtreecommitdiff
path: root/stm/lemmas.mli
AgeCommit message (Expand)Author
2016-09-29Cleanup API, making inference_hook optionalMatthieu Sozeau
2016-09-28Fix bug #4723 and FIXME in API for solve_by_tacMatthieu Sozeau
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-26Pfedit.get_current_context refinement (fix #4523)Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-28Univs: correctly register universe binders for lemmas.Matthieu Sozeau
2015-09-08More potentialities in proof_terminators.Pierre-Marie Pédrot
2015-08-19Documentation by giving a name to a large type.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-07-10Better handling of the universe context in case of Admitted proof obligations.Matthieu Sozeau
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:45:52 +0000