From d081f9390206c510d9837e2ecd3fa0a0d4ef0b8c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 7 Apr 2014 16:44:02 +0200 Subject: Fix declarations of monomorphic assumptions --- test-suite/success/auto.v | 2 +- 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 -- cgit v1.2.3