aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/sign.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 8c05d15ca2..da6ec5a11d 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -15,7 +15,6 @@ open Term
(*s Signatures of named hypotheses. Used for section variables and
goal assumptions. *)
-type named_declaration = identifier * constr option * types
type named_context = named_declaration list
let empty_named_context = []