Unifying standard "constr_level" names for constructors of local_binder_expr.

RawLocal -> CLocal

5 files changed, 51 insertions, 51 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index c861641010..ee6acde6b2 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -37,10 +37,10 @@ let binder_kind_eq b1 b2 = match b1, b2 with
 let default_binder_kind = Default Explicit
 
 let names_of_local_assums bl =
-  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
+  List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl)
 
 let names_of_local_binders bl =
-  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalRawPattern _ -> assert false) bl)
+  List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_)->[l]|CLocalPattern _ -> assert false) bl)
 
 (**********************************************************************)
 (* Functions on constr_expr *)
@@ -212,9 +212,9 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with
 | _ -> false
 
 and local_binder_eq l1 l2 = match l1, l2 with
-| LocalRawDef (n1, e1), LocalRawDef (n2, e2) ->
+| CLocalDef (n1, e1), CLocalDef (n2, e2) ->
   eq_located Name.equal n1 n2 && constr_expr_eq e1 e2
-| LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) ->
+| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
   (** Don't care about the [binder_kind] *)
   List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
 | _ -> false
@@ -269,10 +269,10 @@ let raw_cases_pattern_expr_loc = function
   | RCPatOr (loc,_) -> loc
 
 let local_binder_loc = function
-  | LocalRawAssum ((loc,_)::_,_,t)
-  | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
-  | LocalRawAssum ([],_,_) -> assert false
-  | LocalRawPattern (loc,_,_) -> loc
+  | CLocalAssum ((loc,_)::_,_,t)
+  | CLocalDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
+  | CLocalAssum ([],_,_) -> assert false
+  | CLocalPattern (loc,_,_) -> loc
 
 let local_binders_loc bll = match bll with
   | [] -> Loc.ghost
@@ -308,17 +308,17 @@ let expand_pattern_binders mkC bl c =
     | b :: bl ->
         let (env, bl, c) = loop bl c in
         match b with
-        | LocalRawDef (n, _) ->
+        | CLocalDef (n, _) ->
             let env = add_name_in_env env n in
             (env, b :: bl, c)
-        | LocalRawAssum (nl, _, _) ->
+        | CLocalAssum (nl, _, _) ->
             let env = List.fold_left add_name_in_env env nl in
             (env, b :: bl, c)
-        | LocalRawPattern (loc, p, ty) ->
+        | CLocalPattern (loc, p, ty) ->
             let ni = Hook.get fresh_var env c in
             let id = (loc, Name ni) in
             let b =
-              LocalRawAssum
+              CLocalAssum
                 ([id], Default Explicit,
                  match ty with
                  | Some ty -> ty
@@ -338,13 +338,13 @@ let expand_pattern_binders mkC bl c =
 let mkCProdN loc bll c =
   let rec loop loc bll c =
     match bll with
-    | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+    | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
         CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
-    | LocalRawDef ((loc1,_) as id,b) :: bll ->
+    | CLocalDef ((loc1,_) as id,b) :: bll ->
         CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
     | [] -> c
-    | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
-    | LocalRawPattern (loc,p,ty) :: bll -> assert false
+    | CLocalAssum ([],_,_) :: bll -> loop loc bll c
+    | CLocalPattern (loc,p,ty) :: bll -> assert false
   in
   let (bll, c) = expand_pattern_binders loop bll c in
   loop loc bll c
@@ -352,32 +352,32 @@ let mkCProdN loc bll c =
 let mkCLambdaN loc bll c =
   let rec loop loc bll c =
     match bll with
-    | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+    | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
         CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
-    | LocalRawDef ((loc1,_) as id,b) :: bll ->
+    | CLocalDef ((loc1,_) as id,b) :: bll ->
         CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
     | [] -> c
-    | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
-    | LocalRawPattern (loc,p,ty) :: bll -> assert false
+    | CLocalAssum ([],_,_) :: bll -> loop loc bll c
+    | CLocalPattern (loc,p,ty) :: bll -> assert false
   in
   let (bll, c) = expand_pattern_binders loop bll c in
   loop loc bll c
 
 let rec abstract_constr_expr c = function
   | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
-  | LocalRawAssum (idl,bk,t)::bl ->
+  | CLocalDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+  | CLocalAssum (idl,bk,t)::bl ->
       List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
       (abstract_constr_expr c bl)
-  | LocalRawPattern _::_ -> assert false
+  | CLocalPattern _::_ -> assert false
 
 let rec prod_constr_expr c = function
   | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
-  | LocalRawAssum (idl,bk,t)::bl ->
+  | CLocalDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+  | CLocalAssum (idl,bk,t)::bl ->
       List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
       (prod_constr_expr c bl)
-  | LocalRawPattern _::_ -> assert false
+  | CLocalPattern _::_ -> assert false
 
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8e0f5678ce..b6aacb5ea5 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -821,20 +821,20 @@ and extern_local_binder scopes vars = function
       let (assums,ids,l) =
         extern_local_binder scopes (name_fold Id.Set.add na vars) l in
       (assums,na::ids,
-       LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l)
+       CLocalDef((Loc.ghost,na), extern false scopes vars bd) :: l)
 
   | (Inl na,bk,None,ty)::l ->
       let ty = extern_typ scopes vars ty in
       (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
-          (assums,ids,LocalRawAssum(nal,k,ty')::l)
+          (assums,ids,CLocalAssum(nal,k,ty')::l)
             when constr_expr_eq ty ty' &&
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::assums,na::ids,
-               LocalRawAssum((Loc.ghost,na)::nal,k,ty')::l)
+               CLocalAssum((Loc.ghost,na)::nal,k,ty')::l)
         | (assums,ids,l) ->
             (na::assums,na::ids,
-             LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l))
+             CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l))
 
   | (Inr p,bk,Some bd,ty)::l -> assert false
 
@@ -843,7 +843,7 @@ and extern_local_binder scopes vars = function
         if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
       let p = extern_cases_pattern vars p in
       let (assums,ids,l) = extern_local_binder scopes vars l in
-      (assums,ids, LocalRawPattern(Loc.ghost,p,ty) :: l)
+      (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l)
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e101fa6aa3..5c90ad402e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -470,11 +470,11 @@ let glob_local_binder_of_extended = function
 let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
 
 let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
-  | LocalRawAssum(nal,bk,ty) ->
+  | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern lvar env nal bk ty in
       let bl' = List.map (fun a -> GLocalAssum a) bl' in
       env, bl' @ bl
-  | LocalRawDef((loc,na as locna),def) ->
+  | CLocalDef((loc,na as locna),def) ->
      let indef = intern env def in
      let term, ty =
        match indef with
@@ -483,7 +483,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
      in
       (push_name_env lvar (impls_term_list indef) env locna,
        (GLocalDef ((loc,(na,Explicit,term,ty))))::bl)
-  | LocalRawPattern (loc,p,ty) ->
+  | CLocalPattern (loc,p,ty) ->
       let tyc =
         match ty with
         | Some ty -> ty
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4caacc08c1..ececce340d 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -104,17 +104,17 @@ let ids_of_names l =
 
 let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) =
   let rec aux bdvars l c = match c with
-      ((LocalRawAssum (n, _, c)) :: tl) ->
+      ((CLocalAssum (n, _, c)) :: tl) ->
 	let bound = ids_of_names n in
 	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
 	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
 
-    | ((LocalRawDef (n, c)) :: tl) ->
+    | ((CLocalDef (n, c)) :: tl) ->
 	let bound = match snd n with Anonymous -> [] | Name n -> [n] in
 	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
 	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
 
-    | LocalRawPattern _ :: tl -> assert false
+    | CLocalPattern _ :: tl -> assert false
     | [] -> bdvars, l
   in aux bound l binders
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index ba29bc49dd..241204fe94 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -89,13 +89,13 @@ let rec fold_constr_expr_binders g f n acc b = function
       f n acc b
 
 let rec fold_local_binders g f n acc b = function
-  | LocalRawAssum (nal,bk,t)::l ->
+  | CLocalAssum (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
       let n' = List.fold_right (name_fold g) nal n in
       f n (fold_local_binders g f n' acc b l) t
-  | LocalRawDef ((_,na),t)::l ->
+  | CLocalDef ((_,na),t)::l ->
       f n (fold_local_binders g f (name_fold g na n) acc b l) t
-  | LocalRawPattern (_,pat,t)::l ->
+  | CLocalPattern (_,pat,t)::l ->
       let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
       Option.fold_left (f n) acc t
   | [] ->
@@ -160,7 +160,7 @@ let split_at_annot bl na =
       end
   | Some (loc, id) ->
       let rec aux acc = function
-	| LocalRawAssum (bls, k, t) as x :: rest ->
+	| CLocalAssum (bls, k, t) as x :: rest ->
             let test (_, na) = match na with
             | Name id' -> Id.equal id id'
             | Anonymous -> false
@@ -171,12 +171,12 @@ let split_at_annot bl na =
             | _ ->
               let ans = match l with
               | [] -> acc
-              | _ -> LocalRawAssum (l, k, t) :: acc
+              | _ -> CLocalAssum (l, k, t) :: acc
               in
-              (List.rev ans, LocalRawAssum (r, k, t) :: rest)
+              (List.rev ans, CLocalAssum (r, k, t) :: rest)
             end
-	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
-        | LocalRawPattern (loc,_,_) :: rest ->
+	| CLocalDef _ as x :: rest -> aux (x :: acc) rest
+        | CLocalPattern (loc,_,_) :: rest ->
             Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
             user_err ~loc 
@@ -196,13 +196,13 @@ let map_binders f g e bl =
 let map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
   let h (e,bl) = function
-      LocalRawAssum(nal,k,ty) ->
-        (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl)
-    | LocalRawDef((loc,na),ty) ->
-        (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl)
-    | LocalRawPattern (loc,pat,t) ->
+      CLocalAssum(nal,k,ty) ->
+        (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
+    | CLocalDef((loc,na),ty) ->
+        (name_fold g na e, CLocalDef((loc,na),f e ty)::bl)
+    | CLocalPattern (loc,pat,t) ->
         let ids = ids_of_pattern pat in
-        (Id.Set.fold g ids e, LocalRawPattern (loc,pat,Option.map (f e) t)::bl) in
+        (Id.Set.fold g ids e, CLocalPattern (loc,pat,Option.map (f e) t)::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)