aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarsolve.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarsolve.ml')
-rw-r--r--pretyping/evarsolve.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index fba154291..e6d1e59b3 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,10 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Sorts
open Util
open CErrors
open Names
-open Term
open Constr
open Environ
open Termops