Reductionops API using EConstr.

1 files changed, 2 insertions, 2 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 12d8e98c43..b830ccefee 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -96,14 +96,14 @@ let head_in indl t gl =
     let ity,_ =
       if !up_to_delta
       then find_mrectype env sigma t
-      else extract_mrectype t
+      else extract_mrectype sigma t
     in List.exists (fun i -> eq_ind (fst i) (fst ity)) indl
   with Not_found -> false
 
 let decompose_these c l =
   Proofview.Goal.enter { enter = begin fun gl ->
   let indl = List.map (fun x -> x, Univ.Instance.empty) l in
-  general_decompose (fun sigma (_,t) -> head_in indl t gl) c
+  general_decompose (fun sigma (_,t) -> head_in indl (EConstr.of_constr t) gl) c
   end }
 
 let decompose_and c =