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

15 files changed, 18 insertions, 18 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4029f6150..9215f9b51 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -21,7 +21,7 @@ open Environ
 open Libnames
 open Impargs
 open Topconstr
-open Rawterm
+open Glob_term
 open Pattern
 open Nametab
 open Notation
@@ -743,7 +743,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
-      let loc = Rawterm.loc_of_glob_constr t in
+      let loc = Glob_term.loc_of_glob_constr t in
       try
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args,argsscopes,argsimpls) = match t,n with
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 979c974ac..033090fc9 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -14,7 +14,7 @@ open Sign
 open Environ
 open Libnames
 open Nametab
-open Rawterm
+open Glob_term
 open Pattern
 open Topconstr
 open Notation
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c097ce43d..4e8d0a621 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -14,7 +14,7 @@ open Nameops
 open Namegen
 open Libnames
 open Impargs
-open Rawterm
+open Glob_term
 open Pattern
 open Pretyping
 open Cases
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index cf9e899a6..59afcd313 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -12,7 +12,7 @@ open Sign
 open Evd
 open Environ
 open Libnames
-open Rawterm
+open Glob_term
 open Pattern
 open Topconstr
 open Termops
@@ -82,7 +82,7 @@ val intern_gen : bool -> evar_map -> env ->
 
 val intern_pattern : env -> cases_pattern_expr ->
   Names.identifier list *
-    ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
+    ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list
 
 val intern_context : bool -> evar_map -> env -> local_binder list -> glob_binder list
 
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 23e17a2d4..e564bd11e 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -11,7 +11,7 @@ open Util
 open Names
 open Nameops
 open Nametab
-open Rawterm
+open Glob_term
 open Topconstr
 open Term
 open Evd
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 231126d44..3c825212f 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -10,7 +10,7 @@ open Util
 open Names
 open Term
 open Libnames
-open Rawterm
+open Glob_term
 open Pattern
 open Topconstr
 open Term
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 864e521bf..b430c000b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -16,7 +16,7 @@ open Environ
 open Nametab
 open Mod_subst
 open Util
-open Rawterm
+open Glob_term
 open Topconstr
 open Libnames
 open Typeclasses
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 4c73edbf7..cb782e0c5 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -14,7 +14,7 @@ open Evd
 open Environ
 open Nametab
 open Mod_subst
-open Rawterm
+open Glob_term
 open Topconstr
 open Util
 open Libnames
@@ -42,7 +42,7 @@ val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t ->
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 
-val implicits_of_rawterm : ?with_products:bool -> Rawterm.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list
+val implicits_of_rawterm : ?with_products:bool -> Glob_term.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list
 
 val combine_params_freevar :
   Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
diff --git a/interp/notation.ml b/interp/notation.ml
index eea8afeef..37c9ddbeb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -15,7 +15,7 @@ open Term
 open Nametab
 open Libnames
 open Summary
-open Rawterm
+open Glob_term
 open Topconstr
 open Ppextend
 (*i*)
diff --git a/interp/notation.mli b/interp/notation.mli
index 290d5f3df..52a7c2b99 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -12,7 +12,7 @@ open Bigint
 open Names
 open Nametab
 open Libnames
-open Rawterm
+open Glob_term
 open Topconstr
 open Ppextend
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 9d20236b8..c143b5710 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -46,7 +46,7 @@ let declare_reserved_type (loc,id) t =
 
 let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table
 
-open Rawterm
+open Glob_term
 
 let rec unloc = function
   | GVar (_,id) -> GVar (dummy_loc,id)
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 1766f77b9..0e43e5283 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -8,7 +8,7 @@
 
 open Util
 open Names
-open Rawterm
+open Glob_term
 open Topconstr
 
 val declare_reserved_type : identifier located -> aconstr -> unit
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 21ea7390b..e4da52a33 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -9,7 +9,7 @@
 open Util
 open Names
 open Topconstr
-open Rawterm
+open Glob_term
 open Nametab
 open Libnames
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 61549cb1f..0e0326808 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -12,7 +12,7 @@ open Util
 open Names
 open Nameops
 open Libnames
-open Rawterm
+open Glob_term
 open Term
 open Mod_subst
 (*i*)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 6e8769b85..b01c35093 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -10,7 +10,7 @@ open Pp
 open Util
 open Names
 open Libnames
-open Rawterm
+open Glob_term
 open Term
 open Mod_subst