diff options
Diffstat (limited to 'vernac/command.ml')
| -rw-r--r-- | vernac/command.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index edd2401c7c..cdc1c88e63 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -560,10 +560,10 @@ let check_named (loc, na) = match na with let check_param = function -| LocalRawDef (na, _) -> check_named na -| LocalRawAssum (nas, Default _, _) -> List.iter check_named nas -| LocalRawAssum (nas, Generalized _, _) -> () -| LocalRawPattern _ -> assert false +| CLocalDef (na, _) -> check_named na +| CLocalAssum (nas, Default _, _) -> List.iter check_named nas +| CLocalAssum (nas, Generalized _, _) -> () +| CLocalPattern _ -> assert false let interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; |