From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 1 Nov 2016 20:53:32 +0100
Subject: Reductionops API using EConstr.

---
 tactics/inv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/inv.ml')

diff --git a/tactics/inv.ml b/tactics/inv.ml
index d1d6178da..0b2d2f0b2 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -443,7 +443,7 @@ let raw_inversion inv_kind id status names =
         let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
         CErrors.user_err  msg
     in
-    let IndType (indf,realargs) = find_rectype env sigma t in
+    let IndType (indf,realargs) = find_rectype env sigma (EConstr.of_constr t) in
     let evdref = ref sigma in
     let (elim_predicate, args) =
       make_inv_predicate env evdref indf realargs id status concl in
-- 
cgit v1.2.3