From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 11 Nov 2016 19:52:48 +0100
Subject: Tacmach API using EConstr.

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

(limited to 'plugins/romega/const_omega.ml')

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 4935fe4bb..f2d91bad3 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -353,7 +353,7 @@ let parse_term t =
 let parse_rel gl t =
   try match destructurate t with
     | Kapp("eq",[typ;t1;t2])
-      when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2)
+      when destructurate (Tacmach.pf_nf gl (EConstr.of_constr typ)) = Kapp("Z",[]) -> Req (t1,t2)
     | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
     | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
     | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
-- 
cgit v1.2.3