Merge tag 'upstream/8.5_beta1+dfsg'

Upstream version 8.5~beta1+dfsg

7 files changed, 0 insertions, 397 deletions

diff --git a/test-suite/bugs/opened/shouldnotfail/1338.v-disabled b/test-suite/bugs/opened/shouldnotfail/1338.v-disabled
deleted file mode 100644
index f383d534..00000000
--- a/test-suite/bugs/opened/shouldnotfail/1338.v-disabled
+++ /dev/null
@@ -1,12 +0,0 @@
-Require Import Omega.
-
-Goal forall x, 0 <= x -> x <= 20 -> 
-x <> 0  
-  -> x <> 1 -> x <> 2 -> x <> 3 -> x <>4 -> x <> 5 -> x <> 6 -> x <> 7 -> x <> 8
--> x <> 9 -> x <> 10 
-  -> x <> 11 -> x <> 12 -> x <> 13 -> x <> 14 -> x <> 15 -> x <> 16 -> x <> 17
--> x <> 18 -> x <> 19 -> x <> 20 -> False.
-Proof.
-  intros.
-  omega.
-Qed.
diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v
deleted file mode 100644
index 1845dd1f..00000000
--- a/test-suite/bugs/opened/shouldnotfail/1501.v
+++ /dev/null
@@ -1,93 +0,0 @@
-Set Implicit Arguments.
-
-
-Require Export Relation_Definitions.
-Require Export Setoid.
-
-
-Section Essais.
-
-(* Parametrized Setoid *)
-Parameter K : Type -> Type.
-Parameter equiv : forall A : Type, K A -> K A -> Prop.
-Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x.
-Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x.
-Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z
--> equiv x z.
-
-(* basic operations *)
-Parameter val : forall A : Type, A -> K A.
-Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B.
-
-Parameter
-  bind_compat :
-    forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B),
-    equiv m1 m2 ->
-    (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2).
-
-(* monad axioms *)
-Parameter
-  bind_val_l :
-    forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a).
-Parameter
-  bind_val_r :
-    forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m.
-Parameter
-  bind_assoc :
-    forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C),
-    equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)).
-
-
-Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
-
-Add Relation K equiv
- reflexivity proved by (@equiv_refl)
- symmetry proved by (@equiv_sym)
- transitivity proved by (@equiv_trans)
- as equiv_rel.
-
-Definition fequiv (A B: Type)  (f g: A -> K B) := forall (x:A), (equiv (f x) (g
-x)).
-
-Lemma fequiv_refl : forall (A B: Type) (f : A -> K B), fequiv f f.
-Proof.
-  unfold fequiv; auto with monad.
-Qed.
-
-Lemma fequiv_sym : forall (A B: Type) (x y : A -> K B), fequiv x y -> fequiv y
-x.
-Proof.
-  unfold fequiv; auto with monad.
-Qed.
-
-Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y ->
-fequiv
-y z -> fequiv x z.
-Proof.
-  unfold fequiv; intros; eapply equiv_trans; auto with monad.
-Qed.
-
-Add Relation (fun (A B:Type) => A -> K B) fequiv
- reflexivity proved by (@fequiv_refl)
- symmetry proved by (@fequiv_sym)
- transitivity proved by (@fequiv_trans)
- as fequiv_rel.
-
-Add Morphism bind
- with signature equiv ==> fequiv ==> equiv
- as bind_mor.
-Proof.
- unfold fequiv; intros; apply bind_compat; auto.
-Qed.
-
-Lemma test:
-  forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B),
- (equiv m1 m2) -> (equiv m2 m3) ->
-   equiv (bind m1 (fun a => bind m2 (fun a' => f a a')))
-         (bind m2 (fun a => bind m3 (fun a' => f a a'))).
-Proof.
-  intros A B m1 m2 m3 f H1 H2.
-  setoid_rewrite H1. (* this works *)
-  setoid_rewrite H2.
-  trivial by equiv_refl.
-Qed.
diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v
deleted file mode 100644
index de77e35d..00000000
--- a/test-suite/bugs/opened/shouldnotfail/1596.v
+++ /dev/null
@@ -1,242 +0,0 @@
-
-Require Import Relations.
-Require Import FSets.
-Require Import Arith.
-
-Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false.
-  destruct b;try tauto.
-Qed.
-
-Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with
-Definition t := (X.t * Y.t)%type.
-  Definition t := (X.t * Y.t)%type.
-
-  Definition eq (xy1:t) (xy2:t) :=
-    let (x1,y1) := xy1 in
-      let (x2,y2) := xy2 in
-        (X.eq x1 x2) /\ (Y.eq y1 y2).
-
-  Definition lt (xy1:t) (xy2:t) :=
-    let (x1,y1) := xy1 in
-      let (x2,y2) := xy2 in
-        (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)).
-
-  Lemma eq_refl : forall (x:t),(eq x x).
-    destruct x.
-    unfold eq.
-    split;[apply X.eq_refl | apply Y.eq_refl].
-  Qed.
-
-  Lemma eq_sym : forall (x y:t),(eq x y)->(eq y x).
-    destruct x;destruct y;unfold eq;intro.
-    elim H;clear H;intros.
-    split;[apply X.eq_sym | apply Y.eq_sym];trivial.
-  Qed.
-
-  Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
-    unfold eq;destruct x;destruct y;destruct z;intros.
-    elim H;clear H;intros.
-    elim H0;clear H0;intros.
-    split;[eapply X.eq_trans | eapply Y.eq_trans];eauto.
-  Qed.
-
-  Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
-    unfold lt;destruct x;destruct y;destruct z;intros.
-    case H;clear H;intro.
-    case H0;clear H0;intro.
-    left.
-    eapply X.lt_trans;eauto.
-    elim H0;clear H0;intros.
-    left.
-    case (X.compare t0 t4);trivial;intros.
-    generalize (X.eq_sym H0);intro.
-    generalize (X.eq_trans e H2);intro.
-    elim (X.lt_not_eq H H3).
-    generalize (X.lt_trans l H);intro.
-    generalize (X.eq_sym H0);intro.
-    elim (X.lt_not_eq H2 H3).
-    elim H;clear H;intros.
-    case H0;clear H0;intro.
-    left.
-    case (X.compare t0 t4);trivial;intros.
-    generalize (X.eq_sym H);intro.
-    generalize (X.eq_trans H2 e);intro.
-    elim (X.lt_not_eq H0 H3).
-    generalize (X.lt_trans H0 l);intro.
-    generalize (X.eq_sym H);intro.
-    elim (X.lt_not_eq H2 H3).
-    elim H0;clear H0;intros.
-    right.
-    split.
-    eauto.
-    eauto.
-  Qed.
-
-  Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
-    unfold lt, eq;destruct x;destruct y;intro;intro.
-    elim H0;clear H0;intros.
-    case H.
-    intro.
-    apply (X.lt_not_eq H2 H0).
-    intro.
-    elim H2;clear H2;intros.
-    apply (Y.lt_not_eq H3 H1).
-  Qed.
-
-  Definition compare : forall (x y:t),(Compare lt eq x y).
-    destruct x;destruct y.
-    case (X.compare t0 t2);intro.
-    apply LT.
-    left;trivial.
-    case (Y.compare t1 t3);intro.
-    apply LT.
-    right.
-    tauto.
-    apply EQ.
-    split;trivial.
-    apply GT.
-    right;auto.
-    apply GT.
-    left;trivial.
-  Defined.
-
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
-End OrderedPair.
-
-Module MessageSpi.
-  Inductive message : Set :=
-  | MNam : nat -> message.
-
-  Definition t := message.
-
-  Fixpoint message_lt (m n:message) {struct m} : Prop :=
-    match (m,n) with
-      | (MNam n1,MNam n2) => n1 < n2
-    end.
-
-  Module Ord <: OrderedType with Definition t := message with Definition eq :=
-@eq message.
-    Definition t := message.
-    Definition eq := @eq message.
-    Definition lt := message_lt.
-
-    Lemma eq_refl : forall (x:t),eq x x.
-      unfold eq;auto.
-    Qed.
-
-    Lemma eq_sym : forall (x y:t),(eq x y )->(eq y x).
-      unfold eq;auto.
-    Qed.
-
-    Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
-      unfold eq;auto;intros;congruence.
-    Qed.
-
-    Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
-      unfold lt.
-      induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros.
-      omega.
-    Qed.
-
-    Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
-      unfold eq;unfold lt.
-      induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate
-H0);injection H0;intros.
-      elim (lt_irrefl n);try omega.
-    Qed.
-
-    Definition compare : forall (x y:t),(Compare lt eq x y).
-      unfold lt, eq.
-      induction x;destruct y;intros;try (apply LT;simpl;trivial;fail);try
-(apply
-GT;simpl;trivial;fail).
-      case (lt_eq_lt_dec n n0);intros;try (case s;clear s;intros).
-      apply LT;trivial.
-      apply EQ;trivial.
-      rewrite e;trivial.
-      apply GT;trivial.
-    Defined.
-
-    Hint Immediate eq_sym.
-    Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
-  End Ord.
-
-  Theorem eq_dec : forall (m n:message),{m=n}+{~(m=n)}.
-    intros.
-    case (Ord.compare m n);intro;[right | left | right];try (red;intro).
-    elim (Ord.lt_not_eq m n);auto.
-    rewrite e;auto.
-    elim (Ord.lt_not_eq n m);auto.
-  Defined.
-End MessageSpi.
-
-Module MessagePair := OrderedPair MessageSpi.Ord MessageSpi.Ord.
-
-Module Type Hedge := FSetInterface.S with Module E := MessagePair.
-
-Module A (H:Hedge).
-  Definition hedge := H.t.
-
-  Definition message_relation := relation MessageSpi.message.
-
-  Definition relation_of_hedge (h:hedge) (m n:MessageSpi.message) := H.In (m,n)
-h.
-
-  Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
-    | SynInc : forall (m n:MessageSpi.message),(h m
-n)->(hedge_synthesis_relation h m n).
-
-  Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message)
-(n:MessageSpi.message) {struct m} : bool :=
-    if H.mem (m,n) h
-      then true
-      else false.
-
-  Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
-(relation_of_hedge h).
-
-  Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
-(m n:MessageSpi.message),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec
-h m n).
-    unfold hedge_synthesis_spec;unfold relation_of_hedge.
-    induction m;simpl;intro.
-    elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
-    apply SynInc;apply H.mem_2;trivial.
-    rewrite H in H0.  (* !! possible here !! *)
-    discriminate H0.
-  Qed.
-End A.
-
-Module B (H:Hedge).
-  Definition hedge := H.t.
-
-  Definition message_relation := relation MessageSpi.t.
-
-  Definition relation_of_hedge (h:hedge) (m n:MessageSpi.t) := H.In (m,n) h.
-
-  Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
-    | SynInc : forall (m n:MessageSpi.t),(h m n)->(hedge_synthesis_relation h m
-n).
-
-  Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t)
-{struct m} : bool :=
-    if H.mem (m,n) h
-      then true
-      else false.
-
-  Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
-(relation_of_hedge h).
-
-  Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
-(m n:MessageSpi.t),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec h m
-n).
-    unfold hedge_synthesis_spec;unfold relation_of_hedge.
-    induction m;simpl;intro.
-    elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
-    apply SynInc;apply H.mem_2;trivial.
-
-    rewrite H in H0. (* !! impossible here !! *)
-    discriminate H0.
-  Qed.
-End B.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/shouldnotfail/1671.v b/test-suite/bugs/opened/shouldnotfail/1671.v
deleted file mode 100644
index d95c2108..00000000
--- a/test-suite/bugs/opened/shouldnotfail/1671.v
+++ /dev/null
@@ -1,12 +0,0 @@
-(* Exemple soumis par Pierre Corbineau (bug #1671) *)
-
-CoInductive hdlist : unit -> Type :=
-| cons : hdlist tt -> hdlist tt.
-
-Variable P : forall bo, hdlist bo -> Prop.
-Variable all : forall bo l, P bo l.
-
-Definition F (l:hdlist tt) : P tt l :=
-match l in hdlist u return P u l with
-| cons (cons l') => all tt _
-end.
diff --git a/test-suite/bugs/opened/shouldnotfail/1811.v b/test-suite/bugs/opened/shouldnotfail/1811.v
deleted file mode 100644
index 037b7cb2..00000000
--- a/test-suite/bugs/opened/shouldnotfail/1811.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Export Bool.
-
-Lemma neg2xor : forall b, xorb true b = negb b.
-Proof. auto. Qed.
-
-Goal forall b1 b2, (negb b1 = b2)  ->  xorb true b1 = b2.
-Proof.
-  intros b1 b2.
-  rewrite neg2xor.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/shouldnotfail/2310.v b/test-suite/bugs/opened/shouldnotfail/2310.v
deleted file mode 100644
index 8d1a5149..00000000
--- a/test-suite/bugs/opened/shouldnotfail/2310.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(* Dependent higher-order hole in "refine" (simplified version) *)
-
-Set Implicit Arguments.
-
-Inductive Nest t := Cons : Nest (prod t t) -> Nest t.
-
-Definition cast A x y Heq P H := @eq_rect A x P H y Heq.
-
-Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
-
-(* This used to raise an anomaly Unknown Meta in 8.2 and 8.3beta.
-   It raises a regular error in 8.3 and almost succeeds with the new
-   proof engine: there are two solutions to a unification problem
-   (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
-   leave P as subgoal or choose itself one solution *)
-
-intros. refine (Cons (cast H _ y)).
diff --git a/test-suite/bugs/opened/shouldnotfail/743.v b/test-suite/bugs/opened/shouldnotfail/743.v
deleted file mode 100644
index f1eee6c1..00000000
--- a/test-suite/bugs/opened/shouldnotfail/743.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Require Import Omega.
-
-Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z.
-Proof.
-  intros. omega.
-Qed.
-
-Lemma foo' : forall n m : nat, n <=  n + n * m.
-Proof.
-  intros. omega.
-Qed.
-