s/raw/glob/g in decl_interp.ml for more consistency

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13757 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 19 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index a75f0e20b7..a2b889fe03 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -21,7 +21,7 @@ open Compat
 
 (* INTERN *)
 
-let raw_app (loc,hd,args) = if args =[] then hd else GApp(loc,hd,args)
+let glob_app (loc,hd,args) = if args =[] then hd else GApp(loc,hd,args)
 
 let intern_justification_items globs =
   Option.map (List.map (intern_constr globs))
@@ -181,14 +181,14 @@ let interp_constr_or_thesis check_sort sigma env = function
     Thesis n -> Thesis n
   | This c -> This (interp_constr check_sort sigma env c)
 
-let abstract_one_hyp inject h raw =
+let abstract_one_hyp inject h glob =
   match h with
       Hvar (loc,(id,None)) ->
-	GProd (dummy_loc,Name id, Explicit, GHole (loc,Evd.BinderType (Name id)), raw)
+	GProd (dummy_loc,Name id, Explicit, GHole (loc,Evd.BinderType (Name id)), glob)
     | Hvar (loc,(id,Some typ)) ->
-	GProd (dummy_loc,Name id, Explicit, fst typ, raw)
+	GProd (dummy_loc,Name id, Explicit, fst typ, glob)
     | Hprop st ->
-	GProd (dummy_loc,st.st_label, Explicit, inject st.st_it, raw)
+	GProd (dummy_loc,st.st_label, Explicit, inject st.st_it, glob)
 
 let glob_constr_of_hyps inject hyps head =
   List.fold_right (abstract_one_hyp inject) hyps head
@@ -244,24 +244,24 @@ let rec glob_of_pat =
 	    add_params (pred n) (GHole(dummy_loc,
 				       Evd.TomatchTypeParameter(ind,n))::q) in
 	    let args = List.map glob_of_pat lpat in
-	      raw_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr),
+	      glob_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr),
 		   add_params mind.Declarations.mind_nparams args)
 
 let prod_one_hyp = function
     (loc,(id,None)) ->
-      (fun raw ->
+      (fun glob ->
 	 GProd (dummy_loc,Name id, Explicit,
-		GHole (loc,Evd.BinderType (Name id)), raw))
+		GHole (loc,Evd.BinderType (Name id)), glob))
   | (loc,(id,Some typ)) ->
-      (fun raw ->
-	 GProd (dummy_loc,Name id, Explicit, fst typ, raw))
+      (fun glob ->
+	 GProd (dummy_loc,Name id, Explicit, fst typ, glob))
 
-let prod_one_id (loc,id) raw =
+let prod_one_id (loc,id) glob =
   GProd (dummy_loc,Name id, Explicit,
-	 GHole (loc,Evd.BinderType (Name id)), raw)
+	 GHole (loc,Evd.BinderType (Name id)), glob)
 
-let let_in_one_alias (id,pat) raw =
-  GLetIn (dummy_loc,Name id, glob_of_pat pat, raw)
+let let_in_one_alias (id,pat) glob =
+  GLetIn (dummy_loc,Name id, glob_of_pat pat, glob)
 
 let rec bind_primary_aliases map pat =
   match pat with
@@ -340,7 +340,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
     let dum_args=
       list_tabulate (fun _ -> GHole (dummy_loc,Evd.QuestionMark (Evd.Define false)))
 	oib.Declarations.mind_nrealargs in
-      raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
+      glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
   let inject = function
       Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp Null)
@@ -412,12 +412,12 @@ let interp_casee sigma env = function
 
 let abstract_one_arg = function
     (loc,(id,None)) ->
-      (fun raw ->
+      (fun glob ->
 	 GLambda (dummy_loc,Name id, Explicit,
-		GHole (loc,Evd.BinderType (Name id)), raw))
+		GHole (loc,Evd.BinderType (Name id)), glob))
   | (loc,(id,Some typ)) ->
-      (fun raw ->
-	 GLambda (dummy_loc,Name id, Explicit, fst typ, raw))
+      (fun glob ->
+	 GLambda (dummy_loc,Name id, Explicit, fst typ, glob))
 
 let glob_constr_of_fun args body =
   List.fold_right abstract_one_arg args (fst body)