Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 46 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/shouldsucceed/2404.v
new file mode 100644
index 00000000..fe8eba54
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2404.v
@@ -0,0 +1,46 @@
+(* Check that dependencies in the indices of the type of the terms to
+   match are taken into account and correctly generalized *)
+
+Require Import Relations.Relation_Definitions.
+Require Import Basics.
+
+Record Base := mkBase
+ {(* Primitives *)
+    World : Set
+  (* Names are real, links are theoretical *)
+  ; Name : World -> Set
+
+  ; wweak : World -> World -> Prop
+
+  ; exportw : forall a b : World, (wweak a b) -> (Name b) -> option (Name a)
+}.
+
+Section Derived.
+  Variable base : Base.
+  Definition bWorld := World base.
+  Definition bName  := Name base.
+  Definition bexportw := exportw base.
+  Definition bwweak := wweak base.
+
+  Implicit Arguments bexportw [a b].
+
+Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type :=
+  starReflS : forall a, RstarSetProof T a a
+| starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k.
+
+Implicit Arguments starTransS [I T i j k].
+
+Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type :=  (flip (RstarSetProof (flip rel))).
+
+Definition bwweakFlip (b a : bWorld) : Prop := (bwweak a b).
+Definition Rweak : forall a b : bWorld, Type := RstarInv bwweak.
+
+Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) :=
+  match aRWb,y with
+  | starReflS a, y' => Some y'
+  | starTransS i j k jWk jRWi, y' =>
+    match (bexportw jWk y) with
+    | Some x => exportRweak jRWi x
+    | None   => None
+    end
+  end.