aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evarutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evarutil.ml')
-rw-r--r--engine/evarutil.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 38ceed569..648f96035 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -13,7 +13,6 @@ open Util
open Names
open Term
open Constr
-open Pre_env
open Environ
open Evd
open Termops
@@ -876,6 +875,3 @@ let eq_constr_univs_test sigma1 sigma2 t u =
(universes sigma2) fold t u sigma2
in
match ans with None -> false | Some _ -> true
-
-type type_constraint = EConstr.types option
-type val_constraint = EConstr.constr option