aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evardefine.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evardefine.mli')
-rw-r--r--pretyping/evardefine.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index f6d0efba6..f7bf4636b 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -27,7 +27,7 @@ val mk_valcon : EConstr.constr -> val_constraint
[?y[vars1:=args1,vars:=args]] with
[vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *)
val evar_absorb_arguments : env -> evar_map -> EConstr.existential -> EConstr.constr list ->
- evar_map * existential
+ evar_map * EConstr.existential
val split_tycon :
Loc.t -> env -> evar_map -> type_constraint ->