diff options
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/g_nsatz.ml4 | 2 | ||||
| -rw-r--r-- | plugins/nsatz/nsatz.ml | 1 | ||||
| -rw-r--r-- | plugins/nsatz/nsatz.mli | 3 | ||||
| -rw-r--r-- | plugins/nsatz/vo.itarget | 1 |
4 files changed, 4 insertions, 3 deletions
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 7598852531..5a6d72036e 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -8,8 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API open Ltac_plugin -open Names DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 6ba4c0f930..dd1d8764ab 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open CErrors open Util open Term diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli index e876ccfa5d..c0dad72ad6 100644 --- a/plugins/nsatz/nsatz.mli +++ b/plugins/nsatz/nsatz.mli @@ -6,4 +6,5 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val nsatz_compute : Constr.t -> unit Proofview.tactic +open API +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 |