aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.ml
AgeCommit message (Expand)Author
2017-09-19proof_global: cleanup and comment close_proofMatthieu Sozeau
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
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-16Remove Warnings: unused value ...Amin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-12[proof] Move bullets to their own module.Emilio Jesus Gallego Arias
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-24Merge PR#642: Small cleanup on `close_proof` type.Maxime Dénès
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-05-20Change wrong bullet message.Théo Zimmermann
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24Merge PR#552: Miscelaneous commitsMaxime Dénès
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-20COMMENT: Proof_global.pstate.pidMatej Kosik
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-21[pp] [ide] Minor cleanups in pp code.Emilio Jesus Gallego Arias
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-24Fix some documentation typos.Guillaume Melquiond
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-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-25CLEANUP: Type alias "Context.section_context" was removedMatej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-14Add documentation for goal selectors.Cyprien Mangin
2016-06-14Add goal range selectors.Cyprien Mangin
2016-05-10Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Enrico Tassi
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-20Fixing Not_found on unknown bullet behavior.Hugo Herbelin
2016-01-02Use streams rather than strings to handle bullet suggestions.Guillaume Melquiond
2016-01-02Remove some useless module opening.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 14:50:23 +0000