From 767898e6e59e86e3123846374448402360b783e6 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 31 May 2018 12:39:38 +0000 Subject: Allow “Let”-defined coercions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- vernac/class.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac') diff --git a/vernac/class.ml b/vernac/class.ml index 133726702..e425e6474 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -303,12 +303,12 @@ let try_add_new_coercion_with_source ref ~local poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false let add_coercion_hook poly local ref = - let stre = match local with + let local = match local with + | Discharge | Local -> true | Global -> false - | Discharge -> assert false in - let () = try_add_new_coercion ref ~local:stre poly in + let () = try_add_new_coercion ref ~local poly in let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg -- cgit v1.2.3