Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a short econstr-cleaning of record.ml

4 files changed, 17 insertions, 4 deletions

diff --git a/test-suite/bugs/closed/5233.v b/test-suite/bugs/closed/5233.v
new file mode 100644
index 0000000000..06286c740d
--- /dev/null
+++ b/test-suite/bugs/closed/5233.v
@@ -0,0 +1,2 @@
+(* Implicit arguments on type were missing for recursive records *)
+Inductive foo {A : Type} : Type := { Foo : foo }.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f07773f8bd..921433cadd 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -27,3 +27,8 @@ Parameters (a:_) (b:a=0).
 Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
 
 Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
+
+(* Some example which should succeed with local implicit arguments *)
+
+Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A.
+Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P.
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 8334322c99..6f27c1d369 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -87,3 +87,8 @@ Record R : Type := {
   P (A : Type) : Prop := exists x : A -> A, x = x;
   Q A : P A -> P A
 }.
+
+(* We allow reusing an implicit parameter named in non-recursive types *)
+(* This is used in a couple of development such as UniMatch *)
+
+Record S {A:Type} := { a : A; b : forall A:Type, A }.
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
index 5b9265b6a8..05ab913932 100644
--- a/test-suite/success/coindprim.v
+++ b/test-suite/success/coindprim.v
@@ -13,9 +13,10 @@ Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}.
 CoFixpoint ones := {| hd := 1; tl := ones |}.
 CoFixpoint ticks := {| hd := tt; tl := ticks |}.
 
-CoInductive stream_equiv {A} {s : Stream A} {s' : Stream A} : Prop :=
-  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv _ s.(tl) s'.(tl) }.
-Arguments stream_equiv {A} s s'.
+CoInductive stream_equiv {A} (s : Stream A) (s' : Stream A) : Prop :=
+  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv s.(tl) s'.(tl) }.
+Arguments hdeq {A} {s} {s'}.
+Arguments tleq {A} {s} {s'}.
 
 Program CoFixpoint ones_eq : stream_equiv ones ones.(tl) :=
   {| hdeq := eq_refl; tleq := ones_eq |}.
@@ -88,4 +89,4 @@ Lemma eq (x : U) : x = force x.
 Proof.
   Fail destruct x.
 Abort.
-  (* Impossible *)
\ No newline at end of file
+  (* Impossible *)