From ce36c131804cd7fb0a460277d88743c7131c5ed3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 8 Feb 2019 11:28:07 +0100
Subject: [PATCH] Coercion intf fix

---
 pretyping/coercion.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index c954a2a8514a..43d4059785ec 100644
--- 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];