diff options
| -rw-r--r-- | test-suite/success/auto.v | 2 | ||||
| -rw-r--r-- | toplevel/command.ml | 6 |
2 files changed, 6 insertions, 2 deletions
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index 9b691e253c..fb9f8c2182 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -14,7 +14,7 @@ Hint Resolve L. Goal G unit Q -> F (Q tt). intro. - auto. + eauto. Qed. (* Test implicit arguments in "using" clause *) diff --git a/toplevel/command.ml b/toplevel/command.ml index f21c1b30d7..a11e3a2cd3 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -220,7 +220,11 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr local p in - (gr,Univ.UContext.instance ctx,Lib.is_modtype_strict ()) + let inst = + if p (* polymorphic *) then Univ.UContext.instance ctx + else Univ.Instance.empty + in + (gr,inst,Lib.is_modtype_strict ()) let declare_assumptions_hook = ref ignore let set_declare_assumptions_hook = (:=) declare_assumptions_hook |