Eliminating parts of the right-hand side compatibility layer

7 files changed, 12 insertions, 6 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 27398cf65..4d2859fb0 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -15,7 +15,7 @@ let get_inductive dir s =
   Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ()))
 
 let decomp_term sigma (c : Term.constr) =
-  Term.kind_of_term (Termops.strip_outer_cast sigma (EConstr.of_constr c))
+  Term.kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c)))
 
 let lapp c v  = Term.mkApp (Lazy.force c, v)
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a12ef00ec..6295e004e 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -87,6 +87,7 @@ let rec decompose_term env sigma t=
 	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->
        let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in
+       let t = EConstr.Unsafe.to_constr t in
        if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 5de2c4151..e73166be2 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -786,7 +786,7 @@ let rec consider_match may_intro introduced available expected gls =
 
 let consider_tac c hyps gls =
   let c = EConstr.of_constr c in
-  match kind_of_term (strip_outer_cast (project gls) c) with
+  match EConstr.kind (project gls) (strip_outer_cast (project gls) c) with
       Var id ->
 	consider_match false [] [id] hyps gls
     | _ ->
@@ -811,6 +811,9 @@ let rec take_tac wits gls =
 
 (* tactics for define *)
 
+let subst_term sigma c t =
+  EConstr.Unsafe.to_constr (subst_term sigma c t)
+
 let rec build_function sigma args body =
   match args with
       st::rest ->
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e9fd40722..460157130 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -42,11 +42,11 @@ let none = Evd.empty
 
 let type_of env c =
   let polyprop = (lang() == Haskell) in
-  Retyping.get_type_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c)))
+  Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))
 
 let sort_of env c =
   let polyprop = (lang() == Haskell) in
-  Retyping.get_sort_family_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c)))
+  Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))
 
 (*S Generation of flags and signatures. *)
 
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index fb237f29b..205cb282d 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -21,7 +21,8 @@ exception UFAIL of constr*constr
    to the equation set. Raises UFAIL with a pair of  terms
 *)
 
-let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *)
+let strip_outer_cast t =
+  EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *)
 
 let unif t1 t2=
   let evd = Evd.empty in (** FIXME *)
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index dbb5cc2de..f9802ee5e 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -471,6 +471,7 @@ let rec fourier () =
     let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
     let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in
+    let goal = EConstr.Unsafe.to_constr goal in
     let fhyp=Id.of_string "new_hyp_for_fourier" in
     (* si le but est une inéquation, on introduit son contraire,
        et le but à prouver devient False *)
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 09e77598a..04a747fb4 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -183,7 +183,7 @@ type inversion_scheme = {
 
 let i_can't_do_that () = error "Quote: not a simple fixpoint"
 
-let decomp_term gl c = kind_of_term (Termops.strip_outer_cast (Tacmach.New.project gl) (EConstr.of_constr c))
+let decomp_term gl c = kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast (Tacmach.New.project gl) (EConstr.of_constr c)))
 
 (*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ...
   ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive