diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_10888.v | 11 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 6 |
2 files changed, 15 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_10888.v b/test-suite/bugs/closed/bug_10888.v new file mode 100644 index 0000000000..3c2e8011d7 --- /dev/null +++ b/test-suite/bugs/closed/bug_10888.v @@ -0,0 +1,11 @@ + +Module Type T. +Context {A:Type}. +End T. + +Module M(X:T). + Import X. + Check X.A. + Check A. + Definition B := A. +End M. diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 8cf5e3a8b4..5ba8b0ab3c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -247,8 +247,10 @@ let context_nosection sigma ~poly ctx = let entry = Declare.definition_entry ~univs ~types:t b in Declare.DefinitionEntry entry in - (* let local = Declare.ImportNeedQualified in *) - let cst = Declare.declare_constant ~name ~kind ~local:Declare.ImportNeedQualified decl in + let local = if Lib.is_modtype () then Declare.ImportDefaultBehavior + else Declare.ImportNeedQualified + in + let cst = Declare.declare_constant ~name ~kind ~local decl in let () = Declare.assumption_message name in let env = Global.env () in (* why local when is_modtype? *) |