aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.mli
AgeCommit message (Expand)Author
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
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-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-19Merge PR #770: [proof] Move bullets to their own module.Maxime Dénès
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-12[proof] Move bullets to their own module.Emilio Jesus Gallego Arias
2017-05-31[proof] Deprecate "proof mode" APIEmilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-21Remove VernacErrorGaetan Gilbert
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
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-05-10Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Enrico Tassi
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Use streams rather than strings to handle bullet suggestions.Guillaume Melquiond
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-28Univs: correctly register universe binders for lemmas.Matthieu Sozeau
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-18Miscellaneous typos, spacing, US spelling in comments or variable names.Hugo Herbelin
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-09-08Opacifying the proof_terminator type.Pierre-Marie Pédrot
2015-07-29Fixing what seems to be a typo.Hugo Herbelin
2015-06-09STM: states coming from workers have no proof terminators (Close #4246)Enrico Tassi
2015-06-03Admitted does not drop poly-univ constraints (Fix #4244)Enrico Tassi
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-01-12Update headers.Maxime Dénès
2015-01-08Fixed and extend bullet related info/error messages. + doc.Pierre Courtieu
2014-12-28Proof using: call "clear" to remove from sight the vars not selectedEnrico Tassi
2014-12-23Vi2vo: fix handling of univ constraints coming from the bodyEnrico Tassi
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 05:42:01 +0000