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.

---
 plugins/omega/coq_omega.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/omega/coq_omega.ml')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 1afc6500b..d15449aef 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1591,7 +1591,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Eq,[typ;t1;t2]) ->
-		if is_conv typ (Lazy.force coq_nat) then
+		if is_conv (EConstr.of_constr typ) (EConstr.of_constr (Lazy.force coq_nat)) then
                   Tacticals.New.tclTHENLIST [
 		    (generalize_tac
 		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
-- 
cgit v1.2.3