aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.ml
AgeCommit message (Expand)Author
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
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-11Univs: Fix bug #4363, nested abstract.Matthieu Sozeau
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-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Fix LemmaOverloadingMatthieu Sozeau
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-09Remove misleading warning (Close #4365)Enrico Tassi
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: fix handling of side effects/delayed proofsMatthieu Sozeau
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-20Proof: suggest Admitted->Qed only if the proof is really complete (#4349)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-05-29STM/Univ: save initial univs (the ones in the statement) in Proof.proofEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:46:26 +0000