Rename rawterm.ml into glob_term.ml

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

12 files changed, 16 insertions, 16 deletions

diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 6326ced8c..c42f13b04 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -40,7 +40,7 @@ struct
   let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac"
 end
 
-open Rawterm
+open Glob_term
 open SubtacGram
 open Util
 open Pcoq
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 0ea2290db..e614085e4 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -26,7 +26,7 @@ open List
 open Recordops
 open Evarutil
 open Pretype_errors
-open Rawterm
+open Glob_term
 open Evarconv
 open Pattern
 open Vernacexpr
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 5ef6f0f88..4dfdc5875 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -20,7 +20,7 @@ open Sign
 open Reductionops
 open Typeops
 open Type_errors
-open Rawterm
+open Glob_term
 open Retyping
 open Pretype_errors
 open Evarutil
diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index 253eacd36..77537d33a 100644
--- a/plugins/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.mli
@@ -13,7 +13,7 @@ open Term
 open Evd
 open Environ
 open Inductiveops
-open Rawterm
+open Glob_term
 open Evarutil
 (*i*)
 
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 88f88b7f2..0d5f7b86e 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -10,7 +10,7 @@ open Pretyping
 open Evd
 open Environ
 open Term
-open Rawterm
+open Glob_term
 open Topconstr
 open Names
 open Libnames
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index a1159dcaa..a09fa3dcc 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -327,8 +327,8 @@ module Coercion = struct
   let apply_pattern_coercion loc pat p =
     List.fold_left
       (fun pat (co,n) ->
-	 let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in
-	   Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
+	 let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
+	   Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
       pat p
 
   (* raise Not_found if no coercion found *)
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 24fdd679b..794143de4 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -6,7 +6,7 @@ open Libobject
 open Pattern
 open Matching
 open Pp
-open Rawterm
+open Glob_term
 open Sign
 open Tacred
 open Util
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 09cc17328..c7924261a 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -24,7 +24,7 @@ open List
 open Recordops
 open Evarutil
 open Pretype_errors
-open Rawterm
+open Glob_term
 open Evarconv
 open Pattern
 
@@ -81,9 +81,9 @@ let find_with_index x l =
 
 open Vernacexpr
 
-let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.glob_constr = 
+let coqintern_constr evd env : Topconstr.constr_expr -> Glob_term.glob_constr = 
   Constrintern.intern_constr evd env
-let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.glob_constr = 
+let coqintern_type evd env : Topconstr.constr_expr -> Glob_term.glob_constr = 
   Constrintern.intern_type evd env
 
 let env_with_binders env isevars l =
diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
index 2b0c8fda2..fa767790d 100644
--- a/plugins/subtac/subtac_pretyping.mli
+++ b/plugins/subtac/subtac_pretyping.mli
@@ -13,7 +13,7 @@ module Pretyping : Pretyping.S
 val interp :
     Environ.env ->
     Evd.evar_map ref ->
-    Rawterm.glob_constr ->
+    Glob_term.glob_constr ->
     Evarutil.type_constraint -> Term.constr * Term.constr
 
 val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list ->
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index debd4f053..b1c4101ce 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -24,7 +24,7 @@ open List
 open Recordops
 open Evarutil
 open Pretype_errors
-open Rawterm
+open Glob_term
 open Evarconv
 open Pattern
 open Pretyping
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 43b55ca95..48ff28aee 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -249,7 +249,7 @@ let build_dependent_sum l =
 		([intros;
 		  (tclTHENSEQ
 		     [constructor_tac false (Some 1) 1
-			(Rawterm.ImplicitBindings [mkVar n]);
+			(Glob_term.ImplicitBindings [mkVar n]);
 		      cont]);
 		 ])))
 	in
@@ -352,7 +352,7 @@ let destruct_ex ext ex =
       | _ -> [acc]
   in aux ex ext
 
-open Rawterm
+open Glob_term
 
 let id_of_name = function
     Name n -> n
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index 659a67781..8c983377a 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -6,7 +6,7 @@ open Pp
 open Evd
 open Decl_kinds
 open Topconstr
-open Rawterm
+open Glob_term
 open Util
 open Evarutil
 open Names