From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:24:58 +0100 Subject: Unifying standard "constr_level" names for constructors of local_binder_expr. RawLocal -> CLocal --- vernac/command.ml | 8 ++++---- vernac/record.ml | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'vernac') diff --git a/vernac/command.ml b/vernac/command.ml index edd2401c7..cdc1c88e6 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; diff --git a/vernac/record.ml b/vernac/record.ml index 05301b3df..a6c8f8b36 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -108,9 +108,9 @@ let typecheck_params_and_fields def id pl t ps nots fs = | _ -> () in List.iter - (function LocalRawDef (b, _) -> error default_binder_kind b - | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls - | LocalRawPattern (loc,_,_) -> + (function CLocalDef (b, _) -> error default_binder_kind b + | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls + | CLocalPattern (loc,_,_) -> Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in -- cgit v1.2.3