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

13 files changed, 13 insertions, 13 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4fc6c5b350..e00e278cd0 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -18,7 +18,7 @@ open Environ
 open Evd
 open Reduction
 open Reductionops
-open Rawterm
+open Glob_term
 open Pattern
 open Tacred
 open Pretype_errors
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 363cf423b0..af51e67164 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -14,7 +14,7 @@ open Environ
 open Evd
 open Evarutil
 open Mod_subst
-open Rawterm
+open Glob_term
 open Unification
 
 (** {6 The Type of Constructions clausale environments.} *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 90c2335d68..76f3856e35 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -22,7 +22,7 @@ open Logic
 open Reduction
 open Reductionops
 open Tacmach
-open Rawterm
+open Glob_term
 open Pattern
 open Tacexpr
 open Clenv
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 43c7e6e5aa..fdd510831c 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -43,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     try Pretyping.Default.understand_ltac true sigma env ltac_var
 	  (Pretyping.OfType (Some evi.evar_concl)) rawc
     with _ ->
-      let loc = Rawterm.loc_of_glob_constr rawc in
+      let loc = Glob_term.loc_of_glob_constr rawc in
       user_err_loc
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index b800d0d66a..8e7c07135f 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -12,7 +12,7 @@ open Environ
 open Evd
 open Refiner
 open Pretyping
-open Rawterm
+open Glob_term
 
 (** Refinement of existential variables. *)
 
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 3d9fcc5a26..fbf7e78e26 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -73,7 +73,7 @@ module Refinable : sig
       context of a term, the remaining evars are registered to the handle.
       It is the main component of the toplevel refine tactic.*)
   val constr_of_raw : 
-    handle -> bool -> bool -> Rawterm.glob_constr -> Term.constr sensitive
+    handle -> bool -> bool -> Glob_term.glob_constr -> Term.constr sensitive
 
 end
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index ebb6db2132..e256794a76 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -15,7 +15,7 @@ open Term
 open Util
 open Tacexpr
 (* open Decl_expr *)
-open Rawterm
+open Glob_term
 open Genarg
 open Nametab
 open Pattern
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index cf73e0dcac..2b0a10ba39 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -13,7 +13,7 @@ open Libnames
 open Term
 open Util
 open Tacexpr
-open Rawterm
+open Glob_term
 open Genarg
 open Nametab
 open Pattern
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index d150f2a38e..69ef4598d7 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -12,7 +12,7 @@ open Names
 open Term
 open Declarations
 open Libnames
-open Rawterm
+open Glob_term
 open Pattern
 open Reductionops
 open Tacred
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 59b7bbd6ea..ae82153d20 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -10,7 +10,7 @@ open Names
 open Term
 open Closure
 open Pattern
-open Rawterm
+open Glob_term
 open Reductionops
 open Termops
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b9e22ca05a..428c674754 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -10,7 +10,7 @@ open Names
 open Topconstr
 open Libnames
 open Nametab
-open Rawterm
+open Glob_term
 open Util
 open Genarg
 open Pattern
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 116526d617..5bfdba8a49 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -202,7 +202,7 @@ let rename_hyp l       = with_check (rename_hyp_no_check l)
 
 open Pp
 open Tacexpr
-open Rawterm
+open Glob_term
 
 let db_pr_goal sigma g =
   let env = Goal.V82.env sigma g in
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index cb26d7be6f..884a030703 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -16,7 +16,7 @@ open Proof_type
 open Refiner
 open Redexpr
 open Tacexpr
-open Rawterm
+open Glob_term
 open Pattern
 
 (** Operations for handling terms under a local typing context. *)