Coercion intf fix

ggonthier · Feb 8, 2019 · ce36c13 · ce36c13
1 parent 62cf1ad
commit ce36c13
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
@@ -58,7 +58,8 @@ val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool ->
     is coercible to an object of type [t'] adding evar constraints if needed;
     it fails if no coercion exists *)
 val inh_conv_coerces_to : ?loc:Loc.t ->
-  env -> evar_map -> types -> types -> evar_map
+  env -> evar_map -> ?flags:Evarconv.unify_flags ->
+  types -> types -> evar_map
 
 (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
     pattern [pat] typed in [ind1] into a pattern typed in [ind2];