aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-01-25 16:52:00 +0000
committerGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-02-01 16:20:16 +0000
commit5b8b60508d74bfe5e436ce182889ad8ee6ca3983 (patch)
tree3a9bdfb906444e1f041af3e09df0cc49f911839b /intf
parente42f575b22ff2d2a69951227e8c2dd67fd0ab3ee (diff)
[vernac] Mutual theorems (VernacStartTheoremProof) always have names
Diffstat (limited to 'intf')
-rw-r--r--intf/vernacexpr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index d954ae903..8e0fe54c5 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -210,7 +210,7 @@ type typeclass_constraint = name_decl * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
type proof_expr =
- ident_decl option * (local_binder_expr list * constr_expr)
+ ident_decl * (local_binder_expr list * constr_expr)
type syntax_modifier =
| SetItemLevel of string list * Extend.production_level