aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
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