Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

15 files changed, 221 insertions, 0 deletions

diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index d819dc47..56333973 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Section group_morphism.
 
 (* An example with default canonical structures *)
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 4eb2dbe9..ce9050d4 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -5,3 +5,15 @@ Lemma a : forall x:I eq_refl, match x in I a b c return b = b with C => eq_refl
 intro.
 match goal with |- ?c => let x := eval cbv in c in change x end.
 Abort.
+
+Check forall x:I eq_refl, match x in I x return x = x with C => eq_refl end = eq_refl.
+
+(* This is bug #3210 *)
+
+Inductive I' : let X := Set in X :=
+| C' : I'.
+
+Definition foo (x : I') : bool :=
+  match x with
+  C' => true
+  end.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 3d425754..9661b3bf 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -121,3 +121,44 @@ Inductive foo1 : forall p, Prop := cc1 : foo1 0.
 (* Check cross inference of evars from constructors *)
 
 Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0.
+
+(* An example with reduction removing an occurrence of the inductive type in one of its argument *)
+
+Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1).
+
+(* These types were considered as ill-formed before March 2015, while they
+   could be accepted considering that the type IND1 above was accepted *)
+
+Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2).
+
+Inductive IND3 (A:Type) (T:=fun _ : Type->Type => A) := CONS3 : IND3 (T IND3) -> IND3 A.
+
+Inductive IND4 (A:Type) := CONS4 : IND4 ((fun x => A) IND4) -> IND4 A.
+
+(* This type was ok before March 2015 *)
+
+Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IND5 A.
+
+(* An example of nested positivity which was rejected by the kernel
+   before 24 March 2015 (even with Unset Elimination Schemes to avoid
+   the _rect bug) due to the wrong computation of non-recursively
+   uniform parameters in list' *)
+
+Inductive list' (A:Type) (B:=A) :=
+| nil' : list' A
+| cons' : A -> list' B -> list' A.
+
+Inductive tree := node : list' tree -> tree.
+
+(* This type was raising an anomaly when building the _rect scheme,
+   because of a bug in Inductiveops.get_arity in the presence of
+   let-ins and recursively non-uniform parameters. *)
+
+Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A.
+
+(* This type was raising an anomaly when building the _rect scheme,
+   because of a wrong computation of the number of non-recursively
+   uniform parameters when conversion is needed, leading the example to
+   hit the Inductiveops.get_arity bug mentioned above (see #3491) *)
+
+Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 6a488244..25e464d6 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -1,3 +1,5 @@
+Require Eqdep_dec.
+
 (* Check the behaviour of Injection *)
 
 (* Check that Injection tries Intro until *)
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index d316e4a0..e38affd7 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* compile en user    3m39.915s sur cachalot *)
 Require Import Nsatz.
 
diff --git a/test-suite/success/TacticNotation1.v b/test-suite/success/TacticNotation1.v
new file mode 100644
index 00000000..289f2816
--- /dev/null
+++ b/test-suite/success/TacticNotation1.v
@@ -0,0 +1,20 @@
+Module Type S.
+End S.
+
+Module F (E : S).
+
+  Tactic Notation "foo" := idtac.
+
+  Ltac bar := foo.
+
+End F.
+
+Module G (E : S).
+  Module M := F E.
+
+  Lemma Foo : True.
+  Proof.
+  M.bar.
+  Abort.
+
+End G.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 21b829aa..a4ed76c5 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -536,3 +536,13 @@ Goal forall f:nat->nat, (forall P x, P (f x)) -> let x:=f 0 in x = 0.
 intros f H x.
 apply H.
 Qed.
+
+(* Test that occur-check is not too restrictive (see comments of #3141) *)
+Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a):
+  exists x, exists y, X x y.
+Proof.
+intros; eexists; eexists; case H.
+apply (foo ?y).
+Grab Existential Variables.
+exact 0.
+Qed.
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
new file mode 100644
index 00000000..4e0b7bf5
--- /dev/null
+++ b/test-suite/success/coindprim.v
@@ -0,0 +1,52 @@
+Set Primitive Projections.
+
+CoInductive stream A := { hd : A; tl : stream A }.
+
+CoFixpoint ticks : stream unit :=
+  {| hd := tt; tl := ticks |}.
+
+Arguments hd [ A ] s.
+Arguments tl [ A ] s.
+
+CoInductive bisim {A} : stream A -> stream A -> Prop :=
+  | bisims s s' : hd s = hd s' -> bisim (tl s) (tl s') -> bisim s s'.
+
+Lemma bisim_refl {A} (s : stream A) : bisim s s.
+Proof.
+  revert s.
+  cofix aux. intros. constructor. reflexivity. apply aux.
+Defined.
+
+Lemma constr : forall (A : Type) (s : stream A),
+    bisim s (Build_stream _ s.(hd) s.(tl)).
+Proof.
+  intros. constructor. reflexivity. simpl. apply bisim_refl.
+Defined.
+
+Lemma constr' : forall (A : Type) (s : stream A),
+  s = Build_stream _ s.(hd) s.(tl).
+Proof.
+  intros. 
+  Fail destruct s. 
+Abort.
+
+Eval compute in constr _ ticks.
+
+Notation convertible x y := (eq_refl x : x = y).
+
+Fail Check convertible ticks {| hd := hd ticks; tl := tl ticks |}.
+
+CoInductive U := inU
+ { outU : U }.
+
+CoFixpoint u : U :=
+  inU u.
+
+CoFixpoint force (u : U) : U :=
+  inU (outU u).
+
+Lemma eq (x : U) : x = force x.
+Proof.
+  Fail destruct x.
+Abort.
+  (* Impossible *)
\ No newline at end of file
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index dbbd57ae..61e73f85 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Section Foo.
 
 Variable a : nat.
diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
new file mode 100644
index 00000000..b3e41ab1
--- /dev/null
+++ b/test-suite/success/qed_export.v
@@ -0,0 +1,18 @@
+Lemma a : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff.
+exact H.
+Fail Qed exporting a_subproof.
+Qed exporting exported_seff.
+Check ( exported_seff : True ).
+
+Lemma b : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff2.
+exact H.
+Qed.
+
+Fail Check ( exported_seff2 : True ).
+
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 6dcd6592..62249666 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -148,3 +148,13 @@ eexists. intro H.
 rewrite H.
 reflexivity.
 Abort.
+
+(* Check that rewriting within evars still work (was broken in 8.5beta1) *)
+
+
+Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y.
+intros; eexists; eexists.
+rewrite H.
+Undo.
+subst.
+Abort.
diff --git a/test-suite/success/rewrite_dep.v b/test-suite/success/rewrite_dep.v
index fe250ae8..d0aafd38 100644
--- a/test-suite/success/rewrite_dep.v
+++ b/test-suite/success/rewrite_dep.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Import Setoid.
 Require Import Morphisms.
 Require Vector.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index be0d49e0..0465c4b3 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Require Import Setoid.
 
 Parameter A : Set.
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index b5330779..e540ae5f 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* Check that inversion of names of mutual inductive fixpoints works *)
 (* (cf bug #1031) *)
 
diff --git a/test-suite/success/tryif.v b/test-suite/success/tryif.v
new file mode 100644
index 00000000..4394bddb
--- /dev/null
+++ b/test-suite/success/tryif.v
@@ -0,0 +1,50 @@
+Require Import TestSuite.admit.
+
+(** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *)
+Tactic Notation "not" tactic3(tac) :=
+  (tryif tac then fail 0 tac "succeeds" else idtac); (* error if the tactic solved all goals *) [].
+
+(** Test if a tactic succeeds, but always roll-back the results *)
+Tactic Notation "test" tactic3(tac) := tryif not tac then fail 0 tac "fails" else idtac.
+
+Goal Set.
+Proof.
+  not fail.
+  not not idtac.
+  not fail 0.
+  (** Would be nice if we could get [not fail 1] to pass, maybe *)
+  not not admit.
+  not not test admit.
+  not progress test admit.
+  (* test grouping *)
+  not (not idtac; fail).
+  assert True.
+  all:not fail.
+  2:not fail.
+  all:admit.
+Defined.
+
+Goal Set.
+Proof.
+  test idtac.
+  test try fail.
+  test admit.
+  test match goal with |- Set => idtac end.
+  test (idtac; match goal with |- Set => idtac end).
+  (* test grouping *)
+  first [ (test idtac; fail); fail 1 | idtac ].
+  try test fail.
+  try test test fail.
+  test test idtac.
+  test test admit.
+  Fail test fail.
+  test (idtac; []).
+  test (assert True; [|]).
+  (* would be nice, perhaps, if we could catch [fail 1] and not just [fail 0] this *)
+  try ((test fail); fail 1).
+  assert True.
+  all:test idtac.
+  all:test admit.
+  2:test admit.
+  all:admit.
+Defined.