diff options
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/g_nsatz.ml4 | 1 | ||||
| -rw-r--r-- | plugins/nsatz/nsatz.mli | 2 | ||||
| -rw-r--r-- | plugins/nsatz/vo.itarget | 1 |
3 files changed, 1 insertions, 3 deletions
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 589c13907c..5a6d72036e 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 d6eb1b406e..c0dad72ad6 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 diff --git a/plugins/nsatz/vo.itarget b/plugins/nsatz/vo.itarget deleted file mode 100644 index 06fc883431..0000000000 --- a/plugins/nsatz/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Nsatz.vo |