aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-24 02:37:26 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-24 02:37:26 +0200
commit28f8da9489463b166391416de86420c15976522f (patch)
tree5456aa680f6e54f7f7bf71f5c4d99dc4e8709e03 /proofs
parent05add9c71214bebf86f1892c5ad946cdce19009a (diff)
parentc1e9a27d383688e44ba34ada24fe08151cb5846e (diff)
Merge PR#642: Small cleanup on `close_proof` type.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--proofs/proof_global.mli2
2 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 99fab0848..01f883cde 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -82,7 +82,7 @@ type proof_object = {
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
| Proved of Vernacexpr.opacity_flag *
- (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+ Vernacexpr.lident option *
proof_object
type proof_terminator = proof_ending -> unit
type closed_proof = proof_object * proof_terminator
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6bb6f5e2c..e90fb5bc9 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -70,7 +70,7 @@ type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
proof_universes
| Proved of Vernacexpr.opacity_flag *
- (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+ Vernacexpr.lident option *
proof_object
type proof_terminator
type closed_proof = proof_object * proof_terminator