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

22 files changed, 22 insertions, 22 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5115b3e3b..6abcd0314 100644
--- a/pretyping/cases.ml
+++ b/pretyping/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/pretyping/cases.mli b/pretyping/cases.mli
index 015b386a5..1ff5b883e 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -12,7 +12,7 @@ open Term
 open Evd
 open Environ
 open Inductiveops
-open Rawterm
+open Glob_term
 open Evarutil
 
 (** {5 Compilation of pattern-matching } *)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 2d2677ee0..8205a6b2e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -17,7 +17,7 @@ open Libobject
 open Library
 open Term
 open Termops
-open Rawterm
+open Glob_term
 open Decl_kinds
 open Mod_subst
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f10fcbc2c..5503a147a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -73,7 +73,7 @@ module type S = sig
      pattern [pat] typed in [ind1] into a pattern typed in [ind2];
      raises [Not_found] if no coercion found *)
   val inh_pattern_coerce_to :
-    loc  -> Rawterm.cases_pattern -> inductive -> inductive -> Rawterm.cases_pattern
+    loc  -> Glob_term.cases_pattern -> inductive -> inductive -> Glob_term.cases_pattern
 end
 
 module Default = struct
@@ -99,8 +99,8 @@ module Default = 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/pretyping/coercion.mli b/pretyping/coercion.mli
index 24c43e051..5d814b294 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -13,7 +13,7 @@ open Term
 open Sign
 open Environ
 open Evarutil
-open Rawterm
+open Glob_term
 
 module type S = sig
   (** {6 Coercions. } *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 7469111bf..4ff4cd333 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -16,7 +16,7 @@ open Inductive
 open Inductiveops
 open Environ
 open Sign
-open Rawterm
+open Glob_term
 open Nameops
 open Termops
 open Namegen
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index e2644592c..fd16c0013 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -11,7 +11,7 @@ open Names
 open Term
 open Sign
 open Environ
-open Rawterm
+open Glob_term
 open Termops
 open Mod_subst
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 80fb4d94e..ae3f64b9c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1401,7 +1401,7 @@ let check_evars env initial_sigma sigma c =
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
-open Rawterm
+open Glob_term
 
 (* Operations on value/type constraints *)
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 3b95784dd..35932bb8e 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -8,7 +8,7 @@
 
 open Util
 open Names
-open Rawterm
+open Glob_term
 open Term
 open Sign
 open Evd
diff --git a/pretyping/rawterm.ml b/pretyping/glob_term.ml
index deba9a257..deba9a257 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/glob_term.ml
diff --git a/pretyping/rawterm.mli b/pretyping/glob_term.mli
index 95305d58c..95305d58c 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/glob_term.mli
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index b971db135..fc56f31d3 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -14,7 +14,7 @@ open Nameops
 open Termops
 open Reductionops
 open Term
-open Rawterm
+open Glob_term
 open Sign
 open Environ
 open Pattern
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 2217074fe..19c5d156a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -11,7 +11,7 @@ open Names
 open Libnames
 open Nameops
 open Term
-open Rawterm
+open Glob_term
 open Environ
 open Nametab
 open Pp
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index a739a2888..b25637de9 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -16,7 +16,7 @@ open Term
 open Environ
 open Libnames
 open Nametab
-open Rawterm
+open Glob_term
 open Mod_subst
 
 (** {5 Maps of pattern variables} *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index cd2ed76c1..b33157414 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -15,7 +15,7 @@ open Termops
 open Namegen
 open Environ
 open Type_errors
-open Rawterm
+open Glob_term
 open Inductiveops
 
 type pretype_error =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index cdf6b523c..11722bee2 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -12,7 +12,7 @@ open Names
 open Term
 open Sign
 open Environ
-open Rawterm
+open Glob_term
 open Inductiveops
 
 (** {6 The type of errors raised by the pretyper } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bc80296d5..baa783d0c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -40,7 +40,7 @@ open List
 open Recordops
 open Evarutil
 open Pretype_errors
-open Rawterm
+open Glob_term
 open Evarconv
 open Pattern
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 8c0270743..70e1a22fb 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -17,7 +17,7 @@ open Sign
 open Term
 open Environ
 open Evd
-open Rawterm
+open Glob_term
 open Evarutil
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 6aa00c5f2..6e2c0a761 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -12,7 +12,7 @@ Term_dnet
 Recordops
 Evarconv
 Typing
-Rawterm
+Glob_term
 Pattern
 Matching
 Tacred
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 90e0683c0..99776367b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -20,7 +20,7 @@ open Environ
 open Closure
 open Reductionops
 open Cbv
-open Rawterm
+open Glob_term
 open Pattern
 open Matching
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 733f38382..d713eae42 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -12,7 +12,7 @@ open Environ
 open Evd
 open Reductionops
 open Closure
-open Rawterm
+open Glob_term
 open Termops
 open Pattern
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6c17567c3..fd287f3af 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -18,7 +18,7 @@ open Environ
 open Evd
 open Reduction
 open Reductionops
-open Rawterm
+open Glob_term
 open Pattern
 open Evarutil
 open Pretype_errors