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

43 files changed, 116 insertions, 116 deletions

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 6c6dbf0f6..fa6acaeb1 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 d16a26550..3a3f50ac8 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 97277ad58..cee4d7271 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 94c7bac2b..0a2ab571f 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
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 24ec23484..881850365 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -12,7 +12,7 @@ open Unify
 open Rules
 open Util
 open Term
-open Rawterm
+open Glob_term
 open Tacmach
 open Tactics
 open Tacticals
@@ -179,12 +179,12 @@ let right_instance_tac inst continue seq=
 	[tclTHENLIST
 	   [introf;
 	    (fun gls->
-	       split (Rawterm.ImplicitBindings
+	       split (Glob_term.ImplicitBindings
 			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
 	 tclTRY assumption]
     | Real ((0,t),_) ->
-	(tclTHEN (split (Rawterm.ImplicitBindings [t]))
+	(tclTHEN (split (Glob_term.ImplicitBindings [t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index e047f13d5..2c5118e92 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -349,9 +349,9 @@ let isLetIn t =
 
 let h_reduce_with_zeta =
   h_reduce
-    (Rawterm.Cbv
-       {Rawterm.all_flags
-	with Rawterm.rDelta = false;
+    (Glob_term.Cbv
+       {Glob_term.all_flags
+	with Glob_term.rDelta = false;
        })
 
 
@@ -963,7 +963,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
 	     [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
-	      (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Rawterm.NoBindings));
+	      (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Glob_term.NoBindings));
 	      intros_reflexivity] g
 	)
       ]
@@ -1399,10 +1399,10 @@ let build_clause eqs =
   {
     Tacexpr.onhyps =
       Some (List.map
-	      (fun id -> (Rawterm.all_occurrences_expr, id), Termops.InHyp)
+	      (fun id -> (Glob_term.all_occurrences_expr, id), Termops.InHyp)
 	      eqs
 	   );
-    Tacexpr.concl_occs = Rawterm.no_occurrences_expr
+    Tacexpr.concl_occs = Glob_term.no_occurrences_expr
   }
 
 let rec rewrite_eqs_in_eqs eqs =
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 6034f19e6..c297f4965 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -501,7 +501,7 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list =
+let make_scheme (fas : (constant*Glob_term.rawsort) list) : Entries.definition_entry list =
   let env = Global.env ()
   and sigma = Evd.empty in
   let funs = List.map fst fas in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index fb04c6ec2..24c8359dc 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -27,8 +27,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
 
 exception No_graph_found
 
-val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list
+val make_scheme : (constant*Glob_term.rawsort) list -> Entries.definition_entry list
 
-val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list ->  unit
-val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort)  ->  unit
+val build_scheme : (identifier*Libnames.reference*Glob_term.rawsort) list ->  unit
+val build_case_scheme : (identifier*Libnames.reference*Glob_term.rawsort)  ->  unit
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 9873d2d5a..90f7b5970 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -19,17 +19,17 @@ open Tacticals
 open Constr
 
 let pr_binding prc = function
-  | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
-  | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+  | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
+  | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
 
 let pr_bindings prc prlc = function
-  | Rawterm.ImplicitBindings l ->
+  | Glob_term.ImplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
       Util.prlist_with_sep spc prc l
-  | Rawterm.ExplicitBindings l ->
+  | Glob_term.ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
         Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
-  | Rawterm.NoBindings -> mt ()
+  | Glob_term.NoBindings -> mt ()
 
 let pr_with_bindings prc prlc (c,bl) =
   prc c ++ hv 0 (pr_bindings prc prlc bl)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index b2b4145d7..6e063d3c1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -4,7 +4,7 @@ open Term
 open Pp
 open Indfun_common
 open Libnames
-open Rawterm
+open Glob_term
 open Declarations
 
 let is_rec_info scheme_info =
@@ -63,7 +63,7 @@ let functional_induction with_clean c princl pat =
 			  errorlabstrm "" (str "Cannot find induction principle for "
 					   ++Printer.pr_lconstr (mkConst c') )
 		    in
-		    (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ)
+		    (princ,Glob_term.NoBindings, Tacmach.pf_type_of g princ)
 		| _ -> raise (UserError("",str "functional induction must be used with a function" ))
 	    end
 	| Some ((princ,binding)) ->
@@ -101,9 +101,9 @@ let functional_induction with_clean c princl pat =
 	    (Tacmach.pf_ids_of_hyps g)
 	in
 	let flag =
-	  Rawterm.Cbv
-	    {Rawterm.all_flags
-	     with Rawterm.rDelta = false;
+	  Glob_term.Cbv
+	    {Glob_term.all_flags
+	     with Glob_term.rDelta = false;
 	    }
 	in
 	Tacticals.tclTHEN
@@ -137,7 +137,7 @@ let interp_casted_constr_with_implicits sigma env impls c  =
     ~allow_patvar:false  ~ltacvars:([],[]) c
 
 (*
-   Construct a fixpoint as a Rawterm
+   Construct a fixpoint as a Glob_term
    and not as a constr
 *)
 
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index f44d12b23..e65b58086 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -4,7 +4,7 @@ open Term
 open Pp
 open Indfun_common
 open Libnames
-open Rawterm
+open Glob_term
 open Declarations
 
 val do_generate_principle :  
@@ -16,7 +16,7 @@ val do_generate_principle :
 val functional_induction :  
   bool ->
   Term.constr ->
-  (Term.constr * Term.constr Rawterm.bindings) option ->
+  (Term.constr * Term.constr Glob_term.bindings) option ->
   Genarg.intro_pattern_expr Util.located option ->
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 9db361cf5..1de0f91d1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -76,8 +76,8 @@ let chop_rlambda_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Rawterm.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
-	  | Rawterm.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
+	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
+	  | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
 	  | _ ->
 	      raise (Util.UserError("chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
@@ -90,7 +90,7 @@ let chop_rprod_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Rawterm.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+	  | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
 	  | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
   chop_prod_n []
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index d802ecf2b..e0076735a 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -35,11 +35,11 @@ val list_union_eq :
 val list_add_set_eq :
   ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
 
-val chop_rlambda_n : int -> Rawterm.glob_constr ->
-  (name*Rawterm.glob_constr*bool) list * Rawterm.glob_constr
+val chop_rlambda_n : int -> Glob_term.glob_constr ->
+  (name*Glob_term.glob_constr*bool) list * Glob_term.glob_constr
 
-val chop_rprod_n : int -> Rawterm.glob_constr ->
-  (name*Rawterm.glob_constr) list * Rawterm.glob_constr
+val chop_rprod_n : int -> Glob_term.glob_constr ->
+  (name*Glob_term.glob_constr) list * Glob_term.glob_constr
 
 val def_of_const : Term.constr -> Term.constr
 val eq : Term.constr Lazy.t
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 24382f875..4e5fb953d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -23,17 +23,17 @@ open Hiddentac
 
 let pr_binding prc  =
   function
-    | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
-    | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
+    | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
+    | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
 
 let pr_bindings prc prlc = function
-  | Rawterm.ImplicitBindings l ->
+  | Glob_term.ImplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
       Util.prlist_with_sep spc prc l
-  | Rawterm.ExplicitBindings l ->
+  | Glob_term.ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
         Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
-  | Rawterm.NoBindings -> mt ()
+  | Glob_term.NoBindings -> mt ()
 
 
 let pr_with_bindings prc prlc (c,bl) =
@@ -312,7 +312,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 		 | None -> (id::pre_args,pre_tac)
 		 | Some b ->
 		     (pre_args,
-		      tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac
+		      tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac
 		     )
 
 	     else (pre_args,pre_tac)
@@ -394,10 +394,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    observe_tac "unfolding" pre_tac;
 	    (* $zeta$ normalizing of the conclusion *)
 	    h_reduce
-	      (Rawterm.Cbv
-		 { Rawterm.all_flags with
-		     Rawterm.rDelta = false ;
-		     Rawterm.rConst = []
+	      (Glob_term.Cbv
+		 { Glob_term.all_flags with
+		     Glob_term.rDelta = false ;
+		     Glob_term.rConst = []
 		 }
 	      )
 	      onConcl;
@@ -423,7 +423,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid
+	     (dummy_loc,Glob_term.NamedHyp id,p)::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
 	  princ_infos.params
@@ -433,12 +433,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
-	     (dummy_loc,Rawterm.NamedHyp id,(nf_zeta p))::bindings,id::avoid)
+	     (dummy_loc,Glob_term.NamedHyp id,(nf_zeta p))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
       in
-      Rawterm.ExplicitBindings (params_bindings@lemmas_bindings)
+      Glob_term.ExplicitBindings (params_bindings@lemmas_bindings)
     in
     tclTHENSEQ
       [ observe_tac "intro args_names" (tclMAP h_intro args_names);
@@ -516,15 +516,15 @@ and intros_with_rewrite_aux : tactic =
 		      Tauto.tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			h_case false (v,Rawterm.NoBindings);
+			h_case false (v,Glob_term.NoBindings);
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
 		      tclTHENSEQ[
 			h_reduce
-			  (Rawterm.Cbv
-			     {Rawterm.all_flags
-			      with Rawterm.rDelta = false;
+			  (Glob_term.Cbv
+			     {Glob_term.all_flags
+			      with Glob_term.rDelta = false;
 			     })
 			  onConcl
 			;
@@ -537,9 +537,9 @@ and intros_with_rewrite_aux : tactic =
 	  | LetIn _ ->
 	      tclTHENSEQ[
 		h_reduce
-		  (Rawterm.Cbv
-		     {Rawterm.all_flags
-		      with Rawterm.rDelta = false;
+		  (Glob_term.Cbv
+		     {Glob_term.all_flags
+		      with Glob_term.rDelta = false;
 		     })
 		  onConcl
 		;
@@ -553,7 +553,7 @@ let rec reflexivity_with_destruct_cases g =
       match kind_of_term (snd (destApp (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      h_case false (v,Rawterm.NoBindings);
+	      h_case false (v,Glob_term.NoBindings);
 	      intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
@@ -676,9 +676,9 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  Equality.rewriteLR (mkConst eq_lemma);
 	  (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *)
 	  h_reduce
-	    (Rawterm.Cbv
-	       {Rawterm.all_flags
-		with Rawterm.rDelta = false;
+	    (Glob_term.Cbv
+	       {Glob_term.all_flags
+		with Glob_term.rDelta = false;
 	       })
 	    onConcl
 	  ;
@@ -723,7 +723,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
 	h_intro graph_principle_id;
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" ((elim false (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
+	  (observe_tac "elim" ((elim false (mkVar hres,Glob_term.NoBindings) (Some (mkVar graph_principle_id,Glob_term.NoBindings)))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
@@ -774,7 +774,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	       (fun entry ->
 		  (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
 	       )
-	       (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs))
+	       (make_scheme (array_map_to_list (fun const -> const,Glob_term.RType None) funs))
 	    )
     in
     let proving_tac =
@@ -945,7 +945,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	    h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
 	    thin [hid];
 	    h_intro hid;
-	    Inv.inv FullInversion None (Rawterm.NamedHyp hid);
+	    Inv.inv FullInversion None (Glob_term.NamedHyp hid);
 	    (fun g ->
 	       let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in
 	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ed8cb9cb6..f757bafcb 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -20,7 +20,7 @@ open Term
 open Termops
 open Declarations
 open Environ
-open Rawterm
+open Glob_term
 open Rawtermops
 
 (** {1 Utilities}  *)
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 7b67e20f3..061600795 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -2,7 +2,7 @@ open Printer
 open Pp
 open Names
 open Term
-open Rawterm
+open Glob_term
 open Libnames
 open Indfun_common
 open Util
@@ -701,7 +701,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
     | GDynamic _ -> error "Not handled GDynamic"
 and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuples)
-    (brl:Rawterm.cases_clauses) avoid :
+    (brl:Glob_term.cases_clauses) avoid :
     glob_constr build_entry_return =
   match el with
     | [] -> assert false (* this case correspond to match <nothing> with .... !*)
@@ -1162,7 +1162,7 @@ and compute_cst_params_from_app acc (params,rtl) =
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
-let compute_params_name relnames (args : (Names.name * Rawterm.glob_constr * bool) list array) csts =
+let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * bool) list array) csts =
   let rels_params =
     Array.mapi
       (fun i args ->
@@ -1233,7 +1233,7 @@ let do_build_inductive
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
     let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-      let rel_first_args :(Names.name * Rawterm.glob_constr * bool ) list  =
+      let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list  =
 	funargs
       in
       List.fold_right
@@ -1299,7 +1299,7 @@ let do_build_inductive
     rel_constructors
   in
   let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-    let rel_first_args :(Names.name * Rawterm.glob_constr * bool ) list  =
+    let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list  =
       (snd (list_chop nrel_params funargs))
     in
     List.fold_right
diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/rawterm_to_relation.mli
index 772e422f8..5c91292ba 100644
--- a/plugins/funind/rawterm_to_relation.mli
+++ b/plugins/funind/rawterm_to_relation.mli
@@ -9,8 +9,8 @@
 
 val build_inductive :
   Names.identifier list -> (* The list of function name *)
-  (Names.name*Rawterm.glob_constr*bool) list list -> (* The list of function args *)
+  (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
   Topconstr.constr_expr list -> (* The list of function returned type *)
-  Rawterm.glob_constr list -> (* the list of body *)
+  Glob_term.glob_constr list -> (* the list of body *)
   unit
 
diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml
index f372fb017..0cf91f38c 100644
--- a/plugins/funind/rawtermops.ml
+++ b/plugins/funind/rawtermops.ml
@@ -1,5 +1,5 @@
 open Pp
-open Rawterm
+open Glob_term
 open Util
 open Names
 (* Ocaml 3.06 Map.S does not handle is_empty *)
diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/rawtermops.mli
index 9e872c236..b6c407a24 100644
--- a/plugins/funind/rawtermops.mli
+++ b/plugins/funind/rawtermops.mli
@@ -1,4 +1,4 @@
-open Rawterm
+open Glob_term
 
 (* Ocaml 3.06 Map.S does not handle is_empty *)
 val idmap_is_empty : 'a Names.Idmap.t -> bool
@@ -73,8 +73,8 @@ val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr
 *)
   val alpha_pat :
     Names.Idmap.key list ->
-    Rawterm.cases_pattern ->
-    Rawterm.cases_pattern * Names.Idmap.key list *
+    Glob_term.cases_pattern ->
+    Glob_term.cases_pattern * Names.Idmap.key list *
       Names.identifier Names.Idmap.t
 
 (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
@@ -84,16 +84,16 @@ val alpha_rt : Names.identifier list -> glob_constr -> glob_constr
 
 (* same as alpha_rt but for case branches *)
 val alpha_br : Names.identifier list ->
-    Util.loc * Names.identifier list * Rawterm.cases_pattern list *
-    Rawterm.glob_constr ->
-    Util.loc * Names.identifier list * Rawterm.cases_pattern list *
-    Rawterm.glob_constr
+    Util.loc * Names.identifier list * Glob_term.cases_pattern list *
+    Glob_term.glob_constr ->
+    Util.loc * Names.identifier list * Glob_term.cases_pattern list *
+    Glob_term.glob_constr
 
 
 (* Reduction function *)
 val replace_var_by_term  :
   Names.identifier ->
-  Rawterm.glob_constr -> Rawterm.glob_constr -> Rawterm.glob_constr
+  Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr
 
 
 
@@ -120,7 +120,7 @@ val ids_of_rawterm: glob_constr -> Names.Idset.t
 (*
    removing let_in construction in a rawterm
 *)
-val zeta_normalize : Rawterm.glob_constr -> Rawterm.glob_constr
+val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr
 
 
 val expand_as : glob_constr -> glob_constr
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1b43d4045..3ab9d58d5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -33,7 +33,7 @@ open Proof_type
 open Vernacinterp
 open Pfedit
 open Topconstr
-open Rawterm
+open Glob_term
 open Pretyping
 open Pretyping.Default
 open Safe_typing
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 68dc7fe0b..20fcd9720 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -19,7 +19,7 @@
 open Quote
 open Ring
 open Mutils
-open Rawterm
+open Glob_term
 open Util
 
 let out_arg = function
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index b235b5821..2b5a3e7c8 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -16,7 +16,7 @@ open Closure
 open Environ
 open Libnames
 open Tactics
-open Rawterm
+open Glob_term
 open Tacticals
 open Tacexpr
 open Pcoq
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 6bdfea4ad..83ecf72ee 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -125,7 +125,7 @@ let intern_id,unintern_id =
 
 let mk_then = tclTHENLIST
 
-let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c])
+let exists_tac c = constructor_tac false (Some 1) 1 (Glob_term.ImplicitBindings [c])
 
 let generalize_tac t = generalize_time (generalize t)
 let elim t = elim_time (simplest_elim t)
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 112a13e53..9a79f2878 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -16,7 +16,7 @@ open Closure
 open Environ
 open Libnames
 open Tactics
-open Rawterm
+open Glob_term
 open Tacticals
 open Tacexpr
 open Pcoq
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
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 50498f0f4..bd2285bb3 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -10,7 +10,7 @@ open Pp
 open Util
 open Names
 open Pcoq
-open Rawterm
+open Glob_term
 open Topconstr
 open Libnames
 open Coqlib
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 3d8860be4..446ae5225 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -14,7 +14,7 @@ open Pp
 open Util
 open Names
 open Coqlib
-open Rawterm
+open Glob_term
 open Libnames
 open Bigint
 open Coqlib
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 892a5595a..19a3c899f 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -10,7 +10,7 @@
 
 open Bigint
 open Libnames
-open Rawterm
+open Glob_term
 
 (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
 
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index fc953e5e5..b9c0bcd6f 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -20,7 +20,7 @@ exception Non_closed_number
 (**********************************************************************)
 
 open Libnames
-open Rawterm
+open Glob_term
 open Bigint
 
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 61643881e..d670f6026 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -13,7 +13,7 @@ open Pcoq
 open Libnames
 open Topconstr
 open Ascii_syntax
-open Rawterm
+open Glob_term
 open Coqlib
 
 exception Non_closed_string
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 81588bced..cf0253d1f 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -21,7 +21,7 @@ exception Non_closed_number
 (**********************************************************************)
 
 open Libnames
-open Rawterm
+open Glob_term
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 let positive_module = ["Coq";"PArith";"BinPos"]
 let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index c8bb308f5..a21a919ad 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -27,7 +27,7 @@ let cprop =
 ;;
 
 let whd_betadeltaiotacprop env _evar_map ty =
- let module R = Rawterm in
+ let module R = Glob_term in
  let module C = Closure in
  let module CR = C.RedFlags in
  (*** CProp is made Opaque ***)