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

---
 vernac/class.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/vernac/class.ml b/vernac/class.ml
index 1337267020..e425e6474d 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