Better test case by PMP for #3948.

1 files changed, 17 insertions, 62 deletions

diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v
index e5bca6e52..165813084 100644
--- a/test-suite/bugs/opened/3948.v
+++ b/test-suite/bugs/opened/3948.v
@@ -1,70 +1,25 @@
-Require Import MSets.
-Require Import Utf8.
-Require FMaps.
-Import Orders.
+Module Type S.
+Parameter t : Type.
+End S.
 
-Set Implicit Arguments.
+Module Bar(X : S).
+Proof.
+  Definition elt := X.t.
+  Axiom fold : elt.
+End Bar.
 
-(* Conversion between the two kinds of OrderedType. *)
-Module OTconvert (O : OrderedType) : OrderedType.OrderedType
-          with Definition t := O.t
-          with Definition eq := O.eq
-          with Definition lt := O.lt.
+Module Make (X: S) := Bar(X).
 
-  Definition t := O.t.
-  Definition eq := O.eq.
-  Definition lt := O.lt.
-  Definition eq_refl := reflexivity.
-  Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-  Admitted.
-  Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-  Admitted.
-  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
-  Admitted.
-  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
-  Admitted.
-  Lemma compare : forall x y : t, OrderedType.Compare lt eq x y.
-  Admitted.
-  Definition eq_dec := O.eq_dec.
-End OTconvert.
+Declare Module X : S.
 
-(* Dependent Maps *)
-Module Type Interface (X : OrderedType).
-  Module Dom : MSetInterface.SetsOn(X) with Definition elt := X.t := MSetAVL.Make(X).
-  Definition key := X.t.
-  Parameter t : forall (A : Type) (dom : Dom.t), Type.
-  Parameter constant : forall A dom, A -> t A dom.
+Module Type Interface.
+  Parameter constant : unit.
 End Interface.
 
-Module DepMap (X : OrderedType) : (Interface X) with Definition key := X.t.
-  Module Dom := MSetAVL.Make(X).
-  Module XOT := OTconvert X.
-  Module S := FMapList.Make(XOT).
-  Definition key := X.t.
-  Definition OK {A} dom (map : S.t A) := ∀ x, S.In x map <-> Dom.In x dom.
-  Definition t := fun A dom => { map : S.t A | OK dom map}.
-  Corollary constant_OK : forall A dom v, OK dom (Dom.fold (fun x m => S.add x v m) dom (S.empty A)).
-  Admitted.
-  Definition constant (A : Type) dom (v : A) : t A dom :=
-    exist (OK dom) (Dom.fold (fun x m => S.add x v m) dom (@S.empty A)) (constant_OK dom v).
+Module DepMap : Interface.
+  Module Dom := Make(X).
+  Definition constant : unit :=
+    let _ := @Dom.fold in tt.
 End DepMap.
 
-
-Declare Module Signal : OrderedType.
-Module S := DepMap(Signal).
-Notation "∅" := (S.constant _ false).
-
-Definition I2Kt {dom} (E : S.t (option bool) dom) : S.t bool dom := S.constant dom false. 
-Arguments I2Kt {dom} E.
-
-Inductive cmd := nothing.
-
-Definition semantics (A T₁ T₂ : Type) := forall dom, T₁ -> S.t A dom -> S.t A dom -> nat -> T₂ -> Prop.
-
-Inductive LBS : semantics bool cmd cmd := LBSnothing dom (E : S.t bool dom) : LBS nothing E ∅ 0 nothing.
-
-Theorem CBS_LBS : forall dom p (E E' : S.t _ dom) k p', LBS p (I2Kt E) (I2Kt E') k p'.
-admit.
-Defined.
-
-Print Assumptions CBS_LBS.
+Print Assumptions DepMap.constant.
\ No newline at end of file