Removing some return type compatibility layers in Termops.

6 files changed, 9 insertions, 7 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 0293842975..f2e98ee011 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -286,7 +286,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     | None ->
 	let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *)
 	let t' = EConstr.Unsafe.to_constr t' in
-	match find_rel (it_mkProd_or_LetIn t' ctx) with
+	match find_rel (Term.it_mkProd_or_LetIn t' ctx) with
 	| Some c -> Some c
 	| None -> None
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3a5347bbfc..b1d5d81350 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1492,7 +1492,7 @@ let _ =
     Used in the partial application tactic. *)
 
 let rec head_of_constr sigma t =
-  let t = strip_outer_cast sigma (EConstr.of_constr (collapse_appl sigma t)) in
+  let t = strip_outer_cast sigma (collapse_appl sigma t) in
     match EConstr.kind sigma t with
     | Prod (_,_,c2)  -> head_of_constr sigma c2
     | LetIn (_,_,_,c2) -> head_of_constr sigma c2
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index a8ea7446fc..e682675843 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -77,7 +77,7 @@ let build_dependent_inductive ind (mib,mip) =
        @ Context.Rel.to_extended_list 0 realargs)
 
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
-let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s
+let my_it_mkProd_or_LetIn s c = Term.it_mkProd_or_LetIn c s
 let my_it_mkLambda_or_LetIn_name s c =
   it_mkLambda_or_LetIn_name (Global.env()) c s
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 231695c35a..d4b73706ce 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1211,7 +1211,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     | Evar (evk,args as ev) ->
       (* We skip the test whether args is the identity or not *)
       let t = existential_type sigma ev in
-      let t = List.fold_right (fun (e,id) c -> EConstr.of_constr (replace_term sigma e id c)) !subst t in
+      let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in
       if not (closed0 sigma c) then
 	error "Hints with holes dependent on a bound variable not supported.";
       if occur_existential sigma t then
@@ -1225,7 +1225,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in
       vars := Id.Set.add id !vars;
       subst := (evar,mkVar id)::!subst;
-      mkNamedLambda id t (iter (EConstr.of_constr (replace_term sigma evar (mkVar id) c))) in
+      mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in
   let c' = iter c in
     if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5ee29c0897..b2f2797a63 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4544,7 +4544,7 @@ let induction_gen_l isrec with_evars elim names lc =
 		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
 
                 let id = new_fresh_id [] x gl in
-		let newl' = List.map (fun r -> EConstr.of_constr (replace_term sigma c (mkVar id) r)) l' in
+		let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
 		let _ = newlc:=id::!newlc in
 		Tacticals.New.tclTHEN
 		  (letin_tac None (Name id) c None allHypsAndConcl)
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 38342b64dc..219abb7fdd 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -350,9 +350,11 @@ struct
     TDnet.Idset.fold
       (fun id acc ->
 	 let c_id = Opt.reduce (Ident.constr_of id) in
+	 let c_id = EConstr.of_constr c_id in
 	 let (ctx,wc) =
-	   try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) (EConstr.of_constr c_id) (** FIXME *)
+	   try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) c_id (** FIXME *)
 	   with Invalid_argument _ -> [],c_id in
+          let wc = EConstr.Unsafe.to_constr wc in
 	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
 	 try
           let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in