diff options
Diffstat (limited to 'vernac/comCoercion.ml')
| -rw-r--r-- | vernac/comCoercion.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 3cc5dd65af..15d8ebc4b5 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -354,7 +354,7 @@ 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 { Declare.Hook.S.scope; dref; _ } = - let open Declare in + let open Locality in let local = match scope with | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) | Global ImportNeedQualified -> true @@ -367,7 +367,7 @@ let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } = let add_coercion_hook ~poly = Declare.Hook.make (add_coercion_hook poly) let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } = - let open Declare in + let open Locality in let stre = match scope with | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) | Global ImportNeedQualified -> true |