Reductionops API using EConstr.

1 files changed, 3 insertions, 3 deletions

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 46f1f7c8d..85910355e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -116,7 +116,7 @@ let max_prefix_sign lid sign =
     | id::l -> snd (max_rec (id, sign_prefix id sign) l)
 *)
 let rec add_prods_sign env sigma t =
-  match kind_of_term (whd_all env sigma t) with
+  match kind_of_term (whd_all env sigma (EConstr.of_constr t)) with
     | Prod (na,c1,b) ->
 	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
@@ -169,7 +169,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
       (pty,goal)
   in
-  let npty = nf_all env sigma pty in
+  let npty = nf_all env sigma (EConstr.of_constr pty) in
   let extenv = push_named (LocalAssum (p,npty)) env in
   extenv, goal
 
@@ -183,7 +183,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
 let inversion_scheme env sigma t sort dep_option inv_op =
   let (env,i) = add_prods_sign env sigma t in
   let ind =
-    try find_rectype env sigma i
+    try find_rectype env sigma (EConstr.of_constr i)
     with Not_found ->
       user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
   in