From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
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 36bce780bd..cc0c4277e5 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


From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 18:18:17 +0100
Subject: Ltac now uses evar-based constrs.

---
 plugins/nsatz/g_nsatz.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 5f906a8dad..a6749c3474 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -13,5 +13,5 @@ DECLARE PLUGIN "nsatz_plugin"
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute"  constr(lt) ] -> [ Nsatz.nsatz_compute lt ]
+| [ "nsatz_compute"  constr(lt) ] -> [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ]
 END
-- 
cgit v1.2.3