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/eqdecide.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/eqdecide.ml')

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 1a67bedc2..1554d43f0 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -197,7 +197,7 @@ let decideGralEquality =
       Proofview.Goal.enter { enter = begin fun gl ->
         let concl = pf_nf_concl gl in
         match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) ->
-        let headtyp = hd_app (pf_compute gl typ) in
+        let headtyp = hd_app (pf_compute gl (EConstr.of_constr typ)) in
         begin match kind_of_term headtyp with
         | Ind (mi,_) -> Proofview.tclUNIT mi
         | _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.")
-- 
cgit v1.2.3