aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarutil.mli')
-rw-r--r--pretyping/evarutil.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 4747bf065..812f3e934 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -89,7 +89,7 @@ val mk_valcon : constr -> val_constraint
val split_tycon :
Rawterm.loc -> env -> evar_defs -> type_constraint ->
- type_constraint * type_constraint
+ name * type_constraint * type_constraint
val valcon_of_tycon : type_constraint -> val_constraint