From 118ae18590dbc7d01cf34e0cd6133b1e34ef9090 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 19 Nov 2016 00:20:30 +0100
Subject: Contradiction API using EConstr.

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

(limited to 'plugins/omega')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 35d763ccc..f39549514 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1092,6 +1092,7 @@ let replay_history tactic_normalisation =
 					Lazy.force coq_Gt;
 					Lazy.force coq_Gt |])
 	    in
+	    let not_sup_sup = EConstr.of_constr not_sup_sup in
             Tacticals.New.tclTHENS
 	      (Tacticals.New.tclTHENLIST [
 		unfold sp_Zle;
-- 
cgit v1.2.3