Hints/Univs: fix bug #4628 anomalies

Fix handling of non-polymorphic hints built from polymorphic values, or
simply producing new universes. We have to record the side effects of
global hints built from constrs which are not polymorphic when they
declare global universes, which might need to be discharged at the end
of sections too. Also issue a warning when a Hint is declared for a
polymorphic reference but the Hint isn't polymorphic itself (this used
to produce an anomaly). For [using] hints, treat all lemmas as
polymorphic, refreshing their universes at each use, as is done for
their existentials (also used to produce an anomaly).

1 files changed, 46 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4628.v b/test-suite/bugs/closed/4628.v
new file mode 100644
index 0000000000..7d4a15d689
--- /dev/null
+++ b/test-suite/bugs/closed/4628.v
@@ -0,0 +1,46 @@
+Module first.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End first.
+
+Module firstbest.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Polymorphic Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End firstbest.
+
+Module second.
+Axiom foo: Set.
+Axiom foo': Set.
+
+Polymorphic Record BAR (A:Type) :=
+  { bar: foo' -> foo}.
+Set Printing Universes.
+
+Lemma baz@{i}: forall (P:BAR@{Set} nat), foo' -> foo.
+  eauto using bar.
+Qed.
+End second.