diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-07 16:44:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:59 +0200 |
| commit | d081f9390206c510d9837e2ecd3fa0a0d4ef0b8c (patch) | |
| tree | ccb55617688c45b934ef6638332a99861324f840 | |
| parent | 2844926420c4a8436ce04711148a717c296c7236 (diff) | |
Fix declarations of monomorphic assumptions
| -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 9b691e253..fb9f8c218 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 f21c1b30d..a11e3a2cd 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 |