Unifying standard "constr_level" names for constructors of local_binder_expr.

RawLocal -> CLocal

4 files changed, 22 insertions, 22 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index de2e5ea4e..2426dd91c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1394,9 +1394,9 @@ let do_build_inductive
       (fun (n,t,is_defined) ->
 	 if is_defined
 	 then
-	   Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t)
+	   Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t)
 	 else
-	 Constrexpr.LocalRawAssum
+	 Constrexpr.CLocalAssum
 	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
       )
       rels_params
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index de2fabb9e..d99c3fa04 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -129,11 +129,11 @@ let functional_induction with_clean c princl pat =
 
 let rec abstract_glob_constr c = function
   | [] -> c
-  | Constrexpr.LocalRawDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl)
-  | Constrexpr.LocalRawAssum (idl,k,t)::bl ->
+  | Constrexpr.CLocalDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl)
+  | Constrexpr.CLocalAssum (idl,k,t)::bl ->
       List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl
         (abstract_glob_constr c bl)
-  | Constrexpr.LocalRawPattern _::bl -> assert false
+  | Constrexpr.CLocalPattern _::bl -> assert false
 
 let interp_casted_constr_with_implicits env sigma impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
@@ -215,9 +215,9 @@ let is_rec names =
 let rec local_binders_length = function
   (* Assume that no `{ ... } contexts occur *)
   | [] -> 0
-  | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl
-  | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
-  | Constrexpr.LocalRawPattern _::bl -> assert false
+  | Constrexpr.CLocalDef _::bl -> 1 + local_binders_length bl
+  | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
+  | Constrexpr.CLocalPattern _::bl -> assert false
 
 let prepare_body ((name,_,args,types,_),_) rt =
   let n = local_binders_length args in
@@ -496,7 +496,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  begin
 	    match args with
-	      | [Constrexpr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x
+	      | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x
 	      | _ -> error "Recursive argument must be specified"
 	  end
       | Some wf_args ->
@@ -504,7 +504,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    match
 	      List.find
 		(function
-		   | Constrexpr.LocalRawAssum(l,k,t) ->
+		   | Constrexpr.CLocalAssum(l,k,t) ->
 		       List.exists
 			 (function (_,Name id) -> Id.equal id wf_args | _ -> false)
 			 l
@@ -512,7 +512,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 		)
 		args
 	    with
-	      | Constrexpr.LocalRawAssum(_,k,t)  ->	    t,wf_args
+	      | Constrexpr.CLocalAssum(_,k,t)  ->	    t,wf_args
 	      | _ -> assert false
 	  with Not_found -> assert false
   in
@@ -570,10 +570,10 @@ let make_assoc assoc l1 l2 =
 let rec rebuild_bl (aux,assoc) bl typ = 
 	match bl,typ with 
 	  | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
-	  | (Constrexpr.LocalRawAssum(nal,bk,_))::bl',typ ->
+	  | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ ->
 	     rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
-	  | (Constrexpr.LocalRawDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') ->
-	    rebuild_bl ((Constrexpr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc)
+	  | (Constrexpr.CLocalDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') ->
+	    rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat)::aux),assoc)
 	      bl' typ'
 	  | _ -> assert false
       and rebuild_nal (aux,assoc) bk bl' nal lnal typ = 
@@ -586,7 +586,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	    then 
 	      let old_nal',new_nal' = List.chop lnal nal' in
 	      let nassoc = make_assoc assoc old_nal' nal in
-	      let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
+	      let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_bl ((assum :: aux), nassoc) bl' 
 		(if List.is_empty new_nal' && List.is_empty rest
 		 then typ'
@@ -596,7 +596,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	    else 
 	      let captured_nal,non_captured_nal = List.chop lnal' nal in
 	      let nassoc = make_assoc assoc nal' captured_nal in
-	      let assum = LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
+	      let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_nal ((assum :: aux), nassoc)
 		bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
 	  | _ -> assert false
@@ -824,7 +824,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
 	  in
 	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
 	  (List.map (fun (nal,k,ta) ->
-		       (Constrexpr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
+		       (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
 	end
     | _ -> [],b,t
 
@@ -865,13 +865,13 @@ let make_graph (f_ref:global_reference) =
 			  List.flatten
 			    (List.map
 			       (function
-				  | Constrexpr.LocalRawDef (na,_)-> []
-				  | Constrexpr.LocalRawAssum (nal,_,_) ->
+				  | Constrexpr.CLocalDef (na,_)-> []
+				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
 					(fun (loc,n) ->
 					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
 					nal
-                                  | Constrexpr.LocalRawPattern _ -> assert false
+                                  | Constrexpr.CLocalPattern _ -> assert false
 			       )
 			       nal_tas
 			    )
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 19c2ed417..7d7c3ad35 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -822,7 +822,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let _ = prNamedRConstr (string_of_name nme) tp in
         let _ = prstr "  ;  " in
         let typ = glob_constr_to_constr_expr tp in
-        LocalRawAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
+        CLocalAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
       [] params in
   let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
   let arity,_ =
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index d286a5870..3e6e2db60 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -70,7 +70,7 @@ GEXTEND Gram
   Constr.closed_binder:
     [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
 	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-          [LocalRawAssum ([id], default_binder_kind, typ)]
+          [CLocalAssum ([id], default_binder_kind, typ)]
     ] ];
 
   END