"Standardizing" the name LocalPatten into LocalRawPattern.

13 files changed, 29 insertions, 29 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 6fbed38fb..7bbf393ac 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -235,7 +235,7 @@ and pp_local_binder lb = (* don't know what it is for now *)
       let ppl =
         List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
       xmlTyped (ppl @ [pp_expr ce])
-  | LocalPattern _ ->
+  | LocalRawPattern _ ->
       assert false
 and pp_local_decl_expr lde = (* don't know what it is for now *)
   match lde with
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)
 
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 0cbb29575..1499ed70e 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -125,7 +125,7 @@ and recursion_order_expr =
 and local_binder =
   | LocalRawDef of Name.t located * constr_expr
   | LocalRawAssum of Name.t located list * binder_kind * constr_expr
-  | LocalPattern of Loc.t * cases_pattern_expr * constr_expr option
+  | LocalRawPattern of Loc.t * cases_pattern_expr * constr_expr option
 
 and constr_notation_substitution =
     constr_expr list *      (** for constr subterms *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 47455f984..bbd494991 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -487,7 +487,7 @@ GEXTEND Gram
             | CPatCast (_, p, ty) -> (p, Some ty)
             | _ -> (p, None)
           in
-          [LocalPattern (!@loc, p, ty)]
+          [LocalRawPattern (!@loc, p, ty)]
     ] ]
   ;
   typeclass_constraint:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 18807113c..666797ba3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -249,7 +249,7 @@ GEXTEND Gram
         | _ -> DefineBody (bl, red, c, None))
     | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
         let ((bl, c), tyo) =
-          if List.exists (function LocalPattern _ -> true | _ -> false) bl
+          if List.exists (function LocalRawPattern _ -> true | _ -> false) bl
           then
             let c = CCast (!@loc, c, CastConv t) in
             (expand_pattern_binders mkCLambdaN bl c, None)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 99b04898b..8d5b1e782 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -133,7 +133,7 @@ let rec abstract_glob_constr c = function
   | Constrexpr.LocalRawAssum (idl,k,t)::bl ->
       List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl
         (abstract_glob_constr c bl)
-  | Constrexpr.LocalPattern _::bl -> assert false
+  | Constrexpr.LocalRawPattern _::bl -> assert false
 
 let interp_casted_constr_with_implicits env sigma impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
@@ -217,7 +217,7 @@ let rec local_binders_length = function
   | [] -> 0
   | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl
   | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
-  | Constrexpr.LocalPattern _::bl -> assert false
+  | Constrexpr.LocalRawPattern _::bl -> assert false
 
 let prepare_body ((name,_,args,types,_),_) rt =
   let n = local_binders_length args in
@@ -871,7 +871,7 @@ let make_graph (f_ref:global_reference) =
 					(fun (loc,n) ->
 					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
 					nal
-                                  | Constrexpr.LocalPattern _ -> assert false
+                                  | Constrexpr.LocalRawPattern _ -> assert false
 			       )
 			       nal_tas
 			    )
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d92d83275..2c2f32209 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -319,7 +319,7 @@ let tag_var = tag Tag.variable
   let begin_of_binder = function
   LocalRawDef((loc,_),_) -> fst (Loc.unloc loc)
     | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
-    | LocalPattern(loc,_,_) -> fst (Loc.unloc loc)
+    | LocalRawPattern(loc,_,_) -> fst (Loc.unloc loc)
     | _ -> assert false
 
   let begin_of_binders = function
@@ -368,7 +368,7 @@ let tag_var = tag Tag.variable
         | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
       surround (pr_lname na ++ pr_opt_type pr_c topt ++
                   str":=" ++ cut() ++ pr_c c)
-    | LocalPattern (loc,p,tyo) ->
+    | LocalRawPattern (loc,p,tyo) ->
       let p = pr_patt lsimplepatt p in
       match tyo with
         | None ->
@@ -384,7 +384,7 @@ let tag_var = tag Tag.variable
     match bl with
       | [LocalRawAssum (nal,k,t)] ->
         kw n ++ pr_binder false pr_c (nal,k,t)
-      | (LocalRawAssum _ | LocalPattern _) :: _ as bdl ->
+      | (LocalRawAssum _ | LocalRawPattern _) :: _ as bdl ->
         kw n ++ pr_undelimited_binders sep pr_c bdl
       | _ -> assert false
 
@@ -402,7 +402,7 @@ let tag_var = tag Tag.variable
               CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_prod_binders b in
-      LocalPattern (loc,p,None) :: bl, c
+      LocalRawPattern (loc,p,None) :: bl, c
     | CProdN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
       LocalRawAssum (nal,bk,t) :: bl, c
@@ -418,7 +418,7 @@ let tag_var = tag Tag.variable
                 CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_lam_binders b in
-      LocalPattern (loc,p,None) :: bl, c
+      LocalRawPattern (loc,p,None) :: bl, c
     | CLambdaN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
       LocalRawAssum (nal,bk,t) :: bl, c
@@ -469,7 +469,7 @@ let tag_var = tag Tag.variable
             let names_of_binder = function
               | LocalRawAssum (nal,_,_) -> nal
               | LocalRawDef (_,_) -> []
-              | LocalPattern _ -> assert false
+              | LocalRawPattern _ -> assert false
             in let ids = List.flatten (List.map names_of_binder bl) in
                if List.length ids > 1 then
                  spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
diff --git a/vernac/command.ml b/vernac/command.ml
index 4b4f4d271..264f5f336 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -563,7 +563,7 @@ let check_param = function
 | LocalRawDef (na, _) -> check_named na
 | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
 | LocalRawAssum (nas, Generalized _, _) -> ()
-| LocalPattern _ -> assert false
+| LocalRawPattern _ -> 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 b494430c2..05301b3df 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -110,7 +110,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
       List.iter 
 	(function LocalRawDef (b, _) -> error default_binder_kind b
 	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls
-           | LocalPattern (loc,_,_) ->
+           | LocalRawPattern (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