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

4 files changed, 10 insertions, 10 deletions

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 6c6dbf0f60..fa6acaeb1f 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -93,7 +93,7 @@ type proof_pattern =
      pat_aliases: (Term.constr*Term.types) statement list;
      pat_constr: Term.constr;
      pat_typ: Term.types;
-     pat_pat: Rawterm.cases_pattern;
+     pat_pat: Glob_term.cases_pattern;
      pat_expr: Topconstr.cases_pattern_expr}
 
 type proof_instr =
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index d16a265508..3a3f50ac8a 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -14,7 +14,7 @@ open Tacmach
 open Decl_expr
 open Decl_mode
 open Pretyping.Default
-open Rawterm
+open Glob_term
 open Term
 open Pp
 open Compat
@@ -343,13 +343,13 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
       raw_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) -> Rawterm.GSort(dummy_loc,RProp Null)
+      Thesis (Plain) -> Glob_term.GSort(dummy_loc,RProp Null)
     | Thesis (For rec_occ) ->
 	if not (List.mem rec_occ pat_vars) then
 	  errorlabstrm "suppose it is"
 	    (str "Variable " ++ Nameops.pr_id rec_occ ++
 	       str " does not occur in pattern.");
-	Rawterm.GSort(dummy_loc,RProp Null)
+	Glob_term.GSort(dummy_loc,RProp Null)
     | This (c,_) -> c in
   let term1 = glob_constr_of_hyps inject hyps raw_prop in
   let loc_ids,npatt =
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 97277ad58e..cee4d7271d 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -17,7 +17,7 @@ open Tacinterp
 open Decl_expr
 open Decl_mode
 open Decl_interp
-open Rawterm
+open Glob_term
 open Names
 open Nameops
 open Declarations
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index 94c7bac2b5..0a2ab571ff 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -37,20 +37,20 @@ val execute_cases :
     Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
 
 val tree_of_pats : 
-  identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
   split_tree
 
 val add_branch : 
-  identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val append_branch :
-  identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
   (Names.Idset.t * Decl_mode.split_tree) option ->
   (Names.Idset.t * Decl_mode.split_tree) option
 
 val append_tree :
-  identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val build_dep_clause :   Term.types Decl_expr.statement list ->
@@ -63,7 +63,7 @@ val register_dep_subcase :
     Names.identifier * (int * int) ->
     Environ.env ->
     Decl_mode.per_info ->
-    Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
+    Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
 
 val thesis_for :     Term.constr ->
     Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr