Unifying standard "constr_level" names for constructors of local_binder_expr.

RawLocal -> CLocal

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;