diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-29 08:58:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-29 08:58:40 +0200 |
| commit | e343fb550c3cd452f0646782edd39c9b7a5a992b (patch) | |
| tree | bfa454318b1401a563a0fe9942b511abb7aaadd7 /toplevel | |
| parent | e368bcd7e16fda4d011ad2c960c647c7da72bcb6 (diff) | |
Fixing commit 50237af2.
Indeed, generalized binders are unnamed, because their name is generated on the
fly.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 3 |
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; |