aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz/nsatz.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/nsatz/nsatz.ml4')
-rw-r--r--plugins/nsatz/nsatz.ml421
1 files changed, 0 insertions, 21 deletions
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 4cac90713..34be7244d 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -8,34 +8,13 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Pp
open Errors
open Util
-open Names
open Term
-open Closure
-open Environ
-open Libnames
open Tactics
-open Glob_term
-open Tacticals
-open Tacexpr
-open Pcoq
-open Tactic
-open Constr
-open Proof_type
open Coqlib
-open Tacmach
-open Mod_subst
-open Tacinterp
-open Libobject
-open Printer
-open Declare
-open Decl_kinds
-open Entries
open Num
-open Unix
open Utile
(***********************************************************************