aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-29 08:58:40 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-29 08:58:40 +0200
commite343fb550c3cd452f0646782edd39c9b7a5a992b (patch)
treebfa454318b1401a563a0fe9942b511abb7aaadd7
parente368bcd7e16fda4d011ad2c960c647c7da72bcb6 (diff)
Fixing commit 50237af2.
Indeed, generalized binders are unnamed, because their name is generated on the fly.
-rw-r--r--toplevel/command.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6d1ca685e..69c0aaea8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -463,7 +463,8 @@ let check_named (loc, na) = match na with
let check_param = function
| LocalRawDef (na, _) -> check_named na
-| LocalRawAssum (nas, _, _) -> List.iter check_named nas
+| LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
+| LocalRawAssum (nas, Generalized _, _) -> ()
let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
check_all_names_different indl;