"Standardizing" the name LocalPatten into LocalRawPattern.

5 files changed, 14 insertions, 14 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 59c24900d..c86164101 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -40,7 +40,7 @@ let names_of_local_assums bl =
   List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
 
 let names_of_local_binders bl =
-  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> assert false) bl)
+  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalRawPattern _ -> assert false) bl)
 
 (**********************************************************************)
 (* Functions on constr_expr *)
@@ -272,7 +272,7 @@ let local_binder_loc = function
   | LocalRawAssum ((loc,_)::_,_,t)
   | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
   | LocalRawAssum ([],_,_) -> assert false
-  | LocalPattern (loc,_,_) -> loc
+  | LocalRawPattern (loc,_,_) -> loc
 
 let local_binders_loc bll = match bll with
   | [] -> Loc.ghost
@@ -314,7 +314,7 @@ let expand_pattern_binders mkC bl c =
         | LocalRawAssum (nl, _, _) ->
             let env = List.fold_left add_name_in_env env nl in
             (env, b :: bl, c)
-        | LocalPattern (loc, p, ty) ->
+        | LocalRawPattern (loc, p, ty) ->
             let ni = Hook.get fresh_var env c in
             let id = (loc, Name ni) in
             let b =
@@ -344,7 +344,7 @@ let mkCProdN loc bll c =
         CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
     | [] -> c
     | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
-    | LocalPattern (loc,p,ty) :: bll -> assert false
+    | LocalRawPattern (loc,p,ty) :: bll -> assert false
   in
   let (bll, c) = expand_pattern_binders loop bll c in
   loop loc bll c
@@ -358,7 +358,7 @@ let mkCLambdaN loc bll c =
         CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
     | [] -> c
     | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
-    | LocalPattern (loc,p,ty) :: bll -> assert false
+    | LocalRawPattern (loc,p,ty) :: bll -> assert false
   in
   let (bll, c) = expand_pattern_binders loop bll c in
   loop loc bll c
@@ -369,7 +369,7 @@ let rec abstract_constr_expr c = function
   | LocalRawAssum (idl,bk,t)::bl ->
       List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
       (abstract_constr_expr c bl)
-  | LocalPattern _::_ -> assert false
+  | LocalRawPattern _::_ -> assert false
 
 let rec prod_constr_expr c = function
   | [] -> c
@@ -377,7 +377,7 @@ let rec prod_constr_expr c = function
   | LocalRawAssum (idl,bk,t)::bl ->
       List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
       (prod_constr_expr c bl)
-  | LocalPattern _::_ -> assert false
+  | LocalRawPattern _::_ -> assert false
 
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3077231be..8e0f5678c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -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, LocalPattern(Loc.ghost,p,ty) :: l)
+      (assums,ids, LocalRawPattern(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 3ed8733df..e08d01669 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -484,7 +484,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,
        (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl)
-  | LocalPattern (loc,p,ty) ->
+  | LocalRawPattern (loc,p,ty) ->
       let tyc =
         match ty with
         | Some ty -> ty
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 77a8ed680..fe0e8d44b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -114,7 +114,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) =
 	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
 	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
 
-    | LocalPattern _ :: tl -> assert false
+    | LocalRawPattern _ :: tl -> assert false
     | [] -> bdvars, l
   in aux bound l binders
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index fd57b70ca..ba29bc49d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -95,7 +95,7 @@ let rec fold_local_binders g f n acc b = function
       f n (fold_local_binders g f n' acc b l) t
   | LocalRawDef ((_,na),t)::l ->
       f n (fold_local_binders g f (name_fold g na n) acc b l) t
-  | LocalPattern (_,pat,t)::l ->
+  | LocalRawPattern (_,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
   | [] ->
@@ -176,7 +176,7 @@ let split_at_annot bl na =
               (List.rev ans, LocalRawAssum (r, k, t) :: rest)
             end
 	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
-        | LocalPattern (loc,_,_) :: rest ->
+        | LocalRawPattern (loc,_,_) :: rest ->
             Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
             user_err ~loc 
@@ -200,9 +200,9 @@ let map_local_binders f g e bl =
         (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)
-    | LocalPattern (loc,pat,t) ->
+    | LocalRawPattern (loc,pat,t) ->
         let ids = ids_of_pattern pat in
-        (Id.Set.fold g ids e, LocalPattern (loc,pat,Option.map (f e) t)::bl) in
+        (Id.Set.fold g ids e, LocalRawPattern (loc,pat,Option.map (f e) t)::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)