aboutsummaryrefslogtreecommitdiff
path: root/kernel/constr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r--kernel/constr.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 826c7f6437..cf05fe0139 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -23,12 +23,8 @@
Inductive Constructions (CIC) terms together with constructors,
destructors, iterators and basic functions *)
-open Errors
open Util
-open Pp
open Names
-open Univ
-open Esubst
type existential_key = Evar.t