From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

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

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 36bce780b..cc0c4277e 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -625,6 +625,7 @@ let nsatz lpol =
 let return_term t =
   let a =
     mkApp(gen_constant "CC" ["Init";"Logic"] "refl_equal",[|tllp ();t|]) in
+  let a = EConstr.of_constr a in
   generalize [a]
 
 let nsatz_compute t =
-- 
cgit v1.2.3