aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evarutil.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evarutil.mli')
-rw-r--r--engine/evarutil.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 2f85bc733..62288ced4 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Evd
open Environ
open EConstr
@@ -54,11 +54,11 @@ val e_new_evar :
val new_type_evar :
env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
- evar_map * (constr * sorts)
+ evar_map * (constr * Sorts.t)
val e_new_type_evar : env -> evar_map ref ->
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
+ ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t
val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr