diff options
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; |