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 2f7ac4efb..b8134a28c 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -31,7 +31,7 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
evar_map * existential
val split_tycon :
- Loc.t -> env -> evar_map -> type_constraint ->
+ ?loc:Loc.t -> env -> evar_map -> type_constraint ->
evar_map * (Name.t * type_constraint * type_constraint)
val valcon_of_tycon : type_constraint -> val_constraint