diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-05-31 12:39:38 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 15:59:33 +0000 |
| commit | 767898e6e59e86e3123846374448402360b783e6 (patch) | |
| tree | 9890e3383c32bd46f1f8447eda30e22aa992d23c /vernac | |
| parent | 8520cc7a02bedf4f4820ef198550f7cfa2a6454c (diff) | |
Allow “Let”-defined coercions
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/class.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |