From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 plugins/nsatz/g_nsatz.ml4 | 1 -
 plugins/nsatz/nsatz.mli   | 2 +-
 2 files changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 589c13907..5a6d72036 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -10,7 +10,6 @@
 
 open API
 open Ltac_plugin
-open Names
 
 DECLARE PLUGIN "nsatz_plugin"
 
diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli
index d6eb1b406..c0dad72ad 100644
--- a/plugins/nsatz/nsatz.mli
+++ b/plugins/nsatz/nsatz.mli
@@ -7,4 +7,4 @@
 (************************************************************************)
 
 open API
-val nsatz_compute : Constr.t -> unit Proofview.tactic
+val nsatz_compute : Term.constr -> unit Proofview.tactic
-- 
cgit v1.2.3