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, 76 insertions, 76 deletions

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