Add a bunch of reproduction files for bugs.

8 files changed, 436 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/2447.v b/test-suite/bugs/opened/2447.v
new file mode 100644
index 0000000000..eeb38386b2
--- /dev/null
+++ b/test-suite/bugs/opened/2447.v
@@ -0,0 +1,5 @@
+Record t := {x : bool; y : bool; z : bool}.
+
+Goal forall x1 x2 y z,
+  {| x := x1; y := y; z := z |} = {| x := x2; y := y; z := z |} -> x1 = x2.
+intros; congruence.
diff --git a/test-suite/bugs/opened/2572.v-disabled b/test-suite/bugs/opened/2572.v-disabled
new file mode 100644
index 0000000000..3f6c6a0d14
--- /dev/null
+++ b/test-suite/bugs/opened/2572.v-disabled
@@ -0,0 +1,187 @@
+Require Import List.
+Definition is_dec (P:Prop) := {P}+{~P}.
+Definition eq_dec (T:Type) := forall (t1 t2:T), is_dec (t1=t2).
+
+Record Label : Type := mkLabel {
+	LabElem: Type;
+	LabProd: LabElem -> LabElem -> option LabElem;
+	LabBot: LabElem -> Prop;
+	LabError: LabElem -> Prop
+}.
+
+Definition LProd (L1 L2: Label): Label := {|
+	LabElem := LabElem L1 * LabElem L2;
+	LabProd := fun lg ld => let (lg1,lg2) := lg in let (ld1,ld2) := ld in
+	  match LabProd L1 lg1 ld1, LabProd L2 lg2 ld2 with
+	    Some g, Some d => Some (g,d)
+	  | _,_ => None
+	  end;
+	LabBot l := let (l1,l2) := l in LabBot L1 l1 \/ LabBot L2 l2;
+	LabError l := let (l1,l2) := l in LabError L1 l1 \/ LabError L2 l2
+|}.
+
+Definition Lrestrict (L: Label) (S: LabElem L -> bool): Label := {|
+	LabElem := LabElem L;
+	LabProd l1 l2 := if andb (S l1) (S l2) then LabProd L l1 l2 else None;
+	LabBot l := LabBot L l;
+	LabError l := LabError L l
+|}.
+
+Notation "l1 ^* l2" := (LProd l1 l2) (at level 50).
+
+Record LTS(L:Type): Type := mkLTS {
+	State: Type;
+	Init: State -> Prop;
+	Next: State -> L -> State -> Prop
+}.
+Implicit Arguments State.
+Implicit Arguments Init.
+Implicit Arguments Next.
+
+Definition sound L (S: LTS (LabElem L)): Prop :=
+  forall s s' l, Next S s l s' -> ~LabError L l.
+
+Inductive PNext L (S1 S2:LTS (LabElem L)): State S1 * State S2 -> (LabElem L) -> State S1 * State S2 -> Prop :=
+  LNext: forall s1 s2 l1 s'1, Next S1 s1 l1 s'1 -> (forall l2, LabProd L l1 l2 = None) ->
+	PNext L S1 S2 (s1,s2) l1 (s'1,s2)
+| RNext: forall s1 s2 l2 s'2, (forall l1, LabProd L l1 l2 = None) -> Next S2 s2 l2 s'2 ->
+	PNext L S1 S2 (s1,s2) l2 (s1,s'2)
+| SNext: forall s1 s2 l1 l2 l s'1 s'2, Next S1 s1 l1 s'1 -> Next S2 s2 l2 s'2 ->
+	Some l = LabProd L l1 l2 -> PNext L S1 S2 (s1,s2) l (s'1,s'2).
+
+Definition Produit (L:Label) (S1 S2: LTS (LabElem L)): LTS (LabElem L) := {|
+	State := State S1 * State S2;
+	Init := fun s => let (s1,s2) := s in Init S1 s1 /\ Init S2 s2;
+	Next :=PNext L S1 S2
+|}.
+
+Parameter Time: Type.
+Parameter teq: forall t1 t2:Time, {t1=t2}+{t1<>t2}.
+
+Inductive TLabElem(L:Type): Type :=
+  Tdiscrete: L -> TLabElem L
+| Tdelay: Time -> TLabElem L
+| Tbot: TLabElem L.
+
+Definition TLabel L: Label := {| 
+    LabElem := TLabElem (LabElem L);
+    LabProd lt1 lt2 :=
+      match lt1, lt2 with
+        Tdiscrete l1, Tdiscrete l2 => match (LabProd L l1 l2) with Some l => Some (Tdiscrete (LabElem L) l) | None => None end
+      | Tdelay t1, Tdelay t2 => if teq t1 t2 then Some (Tdelay (LabElem L) t1) else Some  (Tbot (LabElem L))
+      | _,_ => None
+      end;
+    LabBot lt := match lt with
+      Tdiscrete l => LabBot L l
+        | Tbot => True
+        | _ => False
+    end;
+    LabError lt := match lt with
+      Tdiscrete l => LabError L l
+        | _ => False
+    end
+  |}.
+
+Parameter Var: Type.
+Parameter allv: forall P, (forall (v:Var), is_dec (P v)) -> is_dec (forall v, P v).
+Parameter DType: Type.
+Parameter Data: DType -> Type.
+Parameter vtype: Var -> DType.
+Parameter Deq: forall t (d1 d2: Data t), is_dec (d1=d2).
+
+Inductive Vctr(v:Var): Type :=
+  Wctr: Data (vtype v) -> Vctr v
+| Rctr: Data (vtype v) -> Vctr v
+| Fctr: Vctr v
+| Nctr: Vctr v.
+
+Definition isCmp v (c1 c2: Vctr v): Prop :=
+  match c1,c2 with
+    Wctr _, Nctr => True
+  | Rctr _, Rctr _  => True
+  | Rctr _, Nctr => True
+  | Rctr _, Fctr => True
+  | Nctr, _ => True
+  | _,_ => False
+  end.
+
+Lemma isCmp_dec: forall v (c1 c2: Vctr v), is_dec (isCmp v c1 c2).
+intros.
+induction c1; induction c2; simpl; intros; try (left; tauto); try (right; tauto).
+Qed.
+ 
+Definition Vprod v (c1 c2: Vctr v): (isCmp v c1 c2) -> Vctr v :=
+  match c1,c2 return isCmp v c1 c2 -> Vctr v with
+  | Wctr d, Nctr => fun h => Wctr v d
+  | Rctr d1, Rctr d2 => fun h => if Deq (vtype v) d1 d2 then Rctr v d1 else Fctr v
+  | Rctr d1, Nctr => fun h => Rctr v d1
+  | Rctr d1, Fctr => fun h => Fctr v
+  | Fctr, Rctr _ => fun h => Fctr v
+  | Fctr, Fctr  => fun h => Fctr v
+  | Fctr, Nctr => fun h => Fctr v
+  | Nctr, c2 => fun h => c2
+  | _,_ => fun h => match h with end
+  end.
+
+Inductive MLabElem: Type :=
+  Mctr: (forall v, Vctr v) -> MLabElem
+| Merr: MLabElem.
+
+Definition MProd (m1 m2: MLabElem): MLabElem :=
+  match m1,m2 with
+    Mctr c1, Mctr c2 => match allv (fun v => isCmp v (c1 v) (c2 v)) (fun v => isCmp_dec v (c1 v) (c2 v)) with
+      left h => Mctr (fun v => Vprod v (c1 v) (c2 v)  (h v))
+    | _ => Merr
+    end
+  | _,_ => Merr
+  end.
+
+Definition MLabel: Label := {|
+	LabElem := MLabElem;
+	LabProd m1 m2 := Some (MProd m1 m2);
+	LabBot m := exists c, m = Mctr c /\ exists v, c v = Fctr v;
+	LabError m := m = Merr  
+|}.
+
+Parameter Chan: Type.
+Parameter ch_eq: eq_dec Chan.
+
+Definition CLabel(S: Chan->bool): Label := {|
+	LabElem := Chan;
+	LabProd := fun c1 c2 => if ch_eq c1 c2 then if S c1 then Some c1 else None else None;
+	LabBot := fun _ => False;
+	LabError := fun _ => False
+|}.
+
+Definition FLabel(S: Chan->bool): Label :=
+	TLabel (CLabel S ^* MLabel ^* MLabel ^* MLabel).
+
+Definition FTS := LTS (LabElem (FLabel (fun _ => true))).
+Check (fun S (T1 T2: FTS) => Produit (FLabel S) T1 T2).
+(*
+Definition PAR (S: Chan -> bool) (T1 T2: FTS): FTS.
+unfold FTS in *; simpl in *.
+apply (Produit (FLabel S)).
+apply T1.
+apply T2.
+Defined.
+
+Definition PAR (S: Chan -> bool) (T1 T2: FTS): FTS :=
+	Produit (FLabel S) T1 T2.
+*)
+Lemma FTSirrel (S: Chan -> bool): FTS = LTS (LabElem (FLabel S)).
+Proof.
+ unfold FTS.
+ simpl.
+ reflexivity.
+Qed.
+
+Definition PAR (S: Chan -> bool) (T1 T2: FTS): FTS.
+revert T2; revert T1.
+rewrite (FTSirrel S).
+apply (Produit (FLabel S)).
+Defined.
+
+Record HTTS: Type := mkHTTS {
+	
+}.
diff --git a/test-suite/bugs/opened/2652a.v-disabled b/test-suite/bugs/opened/2652a.v-disabled
new file mode 100644
index 0000000000..0274037b32
--- /dev/null
+++ b/test-suite/bugs/opened/2652a.v-disabled
@@ -0,0 +1,106 @@
+Require Import Strings.String.
+Require Import Classes.EquivDec.
+Require Import Lists.List.
+
+Inductive Owner : Type :=
+ | server : Owner
+ | client : Owner.
+
+Inductive ClassName : Type :=
+ | className : string -> ClassName.
+
+Inductive Label : Type :=
+ | label : nat -> Owner -> Label.
+
+Inductive Var : Type :=
+ | var : string -> Var.
+
+Inductive FieldName : Type :=
+ | fieldName : string -> Owner -> FieldName.
+
+Inductive MethodCall : Type :=
+ | methodCall : string -> MethodCall.
+
+Inductive Exp : Type :=
+ | varExp : Var -> Exp
+ | fieldReference : Var -> FieldName -> Exp
+ | methodCallExp : Var -> MethodCall -> list Var -> Exp
+ | allocation : ClassName -> list Var -> Exp
+ | cast : ClassName -> Var -> Exp.
+
+Inductive Stmt : Type :=
+ | assignment : Var -> Exp -> Label -> Stmt
+ | returnStmt : Var -> Label -> Stmt
+ | fieldUpdate : Var -> FieldName -> Exp -> Label -> Stmt.
+
+Inductive Konst : Type :=
+ | konst : ClassName -> (list (ClassName * FieldName)) -> list FieldName -> (list FieldName * FieldName) -> Konst.
+
+Inductive Method : Type :=
+ | method : ClassName -> MethodCall -> list (ClassName * Var) -> list (ClassName * Var) -> (list Stmt) -> Method.
+
+Inductive Class : Type :=
+ | class : ClassName -> ClassName -> (list (ClassName * FieldName)) -> (Konst * (list Method)) -> Class.
+
+Inductive Context : Type :=
+ | context : nat -> Context.
+
+Inductive HContext : Type :=
+ | heapContext : nat -> HContext.
+
+Inductive Location := loc : nat -> Location.
+
+Definition AbsLocation := ((Var * Context) +  (FieldName * HContext)) % type.
+
+Definition CallStack := list (Stmt * Context * Var) % type.
+
+Inductive TypeState : Type :=
+ | fresh : TypeState
+ | stale : TypeState.
+
+Definition Obj := (HContext * (FieldName -> option AbsLocation) * TypeState) % type.
+
+Definition Store := Location -> option Obj.
+
+Definition OwnerStore := Owner -> Store.
+
+Definition AbsStore := AbsLocation -> option (list Obj).
+
+Definition Stack := list (Var -> option Location).
+
+Definition Batch := list Location.
+
+Definition Sigma := (Stmt * Stack * OwnerStore * AbsStore * CallStack * Context * Batch) % type.
+
+Definition update {A : Type} {B : Type} `{EqDec A} `{EqDec B} (f : A -> B) (k : A) (v : B) : (A -> B) :=
+    fun k' => if equiv_decb k' k then v else f k'.
+  
+
+Definition transfer : Label -> OwnerStore -> Batch -> (OwnerStore * Batch) :=
+  fun _ o b => (o,b).
+
+Parameter succ : Label -> Stmt.
+
+Parameter owner : Label -> Owner.
+
+Inductive concreteSingleStep : Sigma -> Sigma -> Prop :=
+ | fieldAssignmentLocal : forall v f_do  f o  so sigma_so hc m sigma'_so v' l st sigma absSigma cst c b sigma' sigma'' b',
+   (f_do = fieldName f o) -> so = owner(l) -> sigma_so = sigma(so) -> Some (hc, m, fresh) = sigma_so(st(v)) -> sigma'_so = update sigma_so st(v) (Some (hc, update m f_do st(v'), fresh))
+   -> sigma' = update sigma so sigma'_so -> o = so -> (sigma'', b') = transfer l sigma' b ->
+   concreteSingleStep ((fieldUpdate v f_do (varExp v') l), st, sigma, absSigma, cst, c, b)
+                      (succ(l), st, sigma'', absSigma, cst, c, b').
+
+ | fieldAssignmentRemote : forall v f_do  f o  so sigma_so hc m sigma'_so v' l st sigma absSigma cst c b sigma' sigma'' b',
+   (f_do = fieldName f o) -> so = owner(l) -> sigma_so = sigma(so) -> (hc, m, fresh) = sigma_so(st(v)) -> sigma'_so = update sigma_so st(v) (hc, update m f_do st(v'), fresh)
+   -> sigma' = update sigma so sigma'_so -> o <> so -> (sigma'', b') = transfer l sigma' (b ++ st(v)) ->
+   concreteSingleStep ((fieldUpdate v f_o (varExp v') l), st, sigma, absSigma, cst, c, b)
+                      (succ(l), st, sigma'', absSigma, cst, c, b'')
+ | variableStep : forall v v' l st st' sigma sigma' absSigma cst c b b', 
+   (st' = st ++ (update (fun _ => None) v st(v'))) -> (sigma',b') = transfer l sigma b ->
+   concreteSingleStep ((assignment v (varExp v') l), st, sigma, absSigma, cst, c, b) (succ(l), st', sigma', absSigma, cst, c, b')
+ | returnStep : forall v l st sigma absSigma cst c b v_ret s st' sigma' c' b',
+   (s,c',v_ret) = car(cst) -> st' = cdr(st) ++ update (fun _ => None) v_ret st(v) -> (sigma', b') = transfer l sigma b ->
+   concreteSingleStep ((returnStmt v l), st, sigma, absSigma, cst, c, b) (s, st', sigma', absSigma, cdr(cst), c', b')
+ | fieldReferenceStep : forall v v' f_do l st sigma absSigma cst c b so hc m' m st' sigma' absSigma cst c b',
+   so = owner(l) -> (hc, m', fresh) = sigma(so)(st(v')) -> m' = update m f_do l -> st' = st ++ update (fun _ => None) v l -> (sigma', b') = transfer l sigma b ->
+   concreteSingleStep ((assignment v (fieldReference v' f_do) l), st, sigma, absSigma, cst, c, b) (s, st', sigma', absSigma, cst, c, b').
diff --git a/test-suite/bugs/opened/2652b.v-disabled b/test-suite/bugs/opened/2652b.v-disabled
new file mode 100644
index 0000000000..b340436d87
--- /dev/null
+++ b/test-suite/bugs/opened/2652b.v-disabled
@@ -0,0 +1,88 @@
+(* This used to show a bug in evarutil. which is fixed in 8.4 *)
+Require Import Strings.String.
+Require Import Classes.EquivDec.
+Require Import Lists.List.
+
+Inductive Owner : Type :=
+ | server : Owner
+ | client : Owner.
+
+Inductive ClassName : Type :=
+ | className : string -> ClassName.
+
+Inductive Label : Type :=
+ | label : nat -> Owner -> Label.
+
+Inductive Var : Type :=
+ | var : string -> Var.
+
+Inductive FieldName : Type :=
+ | fieldName : string -> Owner -> FieldName.
+
+Inductive MethodCall : Type :=
+ | methodCall : string -> MethodCall.
+
+Inductive Exp : Type :=
+ | varExp : Var -> Exp
+ | fieldReference : Var -> FieldName -> Exp
+ | methodCallExp : Var -> MethodCall -> list Var -> Exp
+ | allocation : ClassName -> list Var -> Exp
+ | cast : ClassName -> Var -> Exp.
+
+Inductive Stmt : Type :=
+ | assignment : Var -> Exp -> Label -> Stmt
+ | returnStmt : Var -> Label -> Stmt
+ | fieldUpdate : Var -> FieldName -> Exp -> Label -> Stmt.
+
+Inductive Konst : Type :=
+ | konst : ClassName -> (list (ClassName * FieldName)) -> list FieldName -> (list FieldName * FieldName) -> Konst.
+
+Inductive Method : Type :=
+ | method : ClassName -> MethodCall -> list (ClassName * Var) -> list (ClassName * Var) -> (list Stmt) -> Method.
+
+Inductive Class : Type :=
+ | class : ClassName -> ClassName -> (list (ClassName * FieldName)) -> (Konst * (list Method)) -> Class.
+
+Inductive Context : Type :=
+ | context : nat -> Context.
+
+Inductive HContext : Type :=
+ | heapContext : nat -> HContext.
+
+Inductive Location := loc : nat -> Location.
+
+Definition AbsLocation := ((Var * Context) +  (FieldName * HContext)) % type.
+
+Definition CallStack := list (Stmt * Context * Var) % type.
+
+Inductive TypeState : Type :=
+ | fresh : TypeState
+ | stale : TypeState.
+
+Definition Obj := (HContext * (FieldName -> option AbsLocation) * TypeState) % type.
+
+Definition Store := Location -> option Obj.
+
+Definition OwnerStore := Owner -> Store.
+
+Definition AbsStore := AbsLocation -> option (list Obj).
+
+Definition Stack := list (Var -> option Location).
+
+Definition Batch := list Location.
+
+Definition Sigma := (Stmt * Stack * OwnerStore * AbsStore * CallStack * Context * Batch) % type.
+
+Definition update {A : Type} {B : Type} `{EqDec A} `{EqDec B} (f : A -> B) (k : A) (v : B) : (A -> B) :=
+    fun k' => if equiv_decb k' k then v else f k'.
+
+Parameter succ : Label -> Stmt.
+
+Inductive concreteSingleStep : Sigma -> Sigma -> Prop :=
+ | fieldAssignmentLocal : forall v f_do  f o  so sigma_so hc m sigma'_so v' l st sigma absSigma cst c b sigma' sigma'' b',
+   Some (hc, m, fresh) = sigma_so(st(v)) -> sigma'_so = update sigma_so st(v) (Some (hc, update m f_do st(v'), fresh))
+   -> 
+   concreteSingleStep ((fieldUpdate v f_do (varExp v') l), st, sigma, absSigma, cst, c, b)
+                      (succ(l), st, sigma'', absSigma, cst, c, b').
+
+.
diff --git a/test-suite/bugs/opened/2800.v b/test-suite/bugs/opened/2800.v
new file mode 100644
index 0000000000..c559ab0c17
--- /dev/null
+++ b/test-suite/bugs/opened/2800.v
@@ -0,0 +1,6 @@
+Goal False.
+
+Fail intuition
+  match goal with
+  | |- _ => idtac " foo"
+  end.
diff --git a/test-suite/bugs/opened/2814.v b/test-suite/bugs/opened/2814.v
new file mode 100644
index 0000000000..d8f6b906a1
--- /dev/null
+++ b/test-suite/bugs/opened/2814.v
@@ -0,0 +1,5 @@
+Require Import Program.
+
+Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False.
+  intros.
+  induction H.
diff --git a/test-suite/bugs/opened/3670.v b/test-suite/bugs/opened/3670.v
new file mode 100644
index 0000000000..cf5e9b090b
--- /dev/null
+++ b/test-suite/bugs/opened/3670.v
@@ -0,0 +1,19 @@
+Module Type FOO.
+  Parameters P Q : Type -> Type.
+End FOO.
+
+Module Type BAR.
+  Declare Module Export foo : FOO.
+  Parameter f : forall A, P A -> Q A -> A.
+End BAR.
+
+Module Type BAZ.
+  Declare Module Export foo : FOO.
+  Parameter g : forall A, P A -> Q A -> A.
+End BAZ.
+
+Module BAR_FROM_BAZ (baz : BAZ) : BAR.
+  Import baz.
+  Module foo <: FOO := foo.
+  Definition f : forall A, P A -> Q A -> A := g.
+End BAR_FROM_BAZ.
diff --git a/test-suite/bugs/opened/3675.v b/test-suite/bugs/opened/3675.v
new file mode 100644
index 0000000000..93227ab852
--- /dev/null
+++ b/test-suite/bugs/opened/3675.v
@@ -0,0 +1,20 @@
+Set Primitive Projections.
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end.
+Notation "p @ q" := (concat p q) (at level 20) : path_scope.
+Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y.
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : forall x, f (equiv_inv x) = x }.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
+Local Open Scope path_scope.
+Local Open Scope equiv_scope.
+Generalizable Variables A B C f g.
+Lemma isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
+: IsEquiv (compose g f).
+Proof.
+  refine (Build_IsEquiv A C
+                        (compose g f)
+                        (compose f^-1 g^-1) _).
+  exact (fun c => ap g (@eisretr _ _ f _ (g^-1 c)) @ (@eisretr _ _ g _ c)).