Merge branch 'trunk' into located_switch

7 files changed, 44 insertions, 153 deletions

diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v
deleted file mode 100644
index a64db4dab7..0000000000
--- a/test-suite/misc/berardi_test.v
+++ /dev/null
@@ -1,153 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This file formalizes Berardi's paradox which says that in
-   the calculus of constructions, excluded middle (EM) and axiom of
-   choice (AC) imply proof irrelevance (PI).
-   Here, the axiom of choice is not necessary because of the use
-   of inductive types.
-<<
-@article{Barbanera-Berardi:JFP96,
-   author    = {F. Barbanera and S. Berardi},
-   title     = {Proof-irrelevance out of Excluded-middle and Choice
-                in the Calculus of Constructions},
-   journal   = {Journal of Functional Programming},
-   year      = {1996},
-   volume    = {6},
-   number    = {3},
-   pages     = {519-525}
-}
->> *)
-
-Set Implicit Arguments.
-
-Section Berardis_paradox.
-
-(** Excluded middle *)
-Hypothesis EM : forall P:Prop, P \/ ~ P.
-
-(** Conditional on any proposition. *)
-Definition IFProp (P B:Prop) (e1 e2:P) :=
-  match EM B with
-  | or_introl _ => e1
-  | or_intror _ => e2
-  end.
-
-(** Axiom of choice applied to disjunction.
-    Provable in Coq because of dependent elimination. *)
-Lemma AC_IF :
- forall (P B:Prop) (e1 e2:P) (Q:P -> Prop),
-   (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).
-Proof.
-intros P B e1 e2 Q p1 p2.
-unfold IFProp.
-case (EM B); assumption.
-Qed.
-
-
-(** We assume a type with two elements. They play the role of booleans.
-    The main theorem under the current assumptions is that [T=F] *)
-Variable Bool : Prop.
-Variable T : Bool.
-Variable F : Bool.
-
-(** The powerset operator *)
-Definition pow (P:Prop) := P -> Bool.
-
-
-(** A piece of theory about retracts *)
-Section Retracts.
-
-Variables A B : Prop.
-
-Record retract : Prop :=
-  {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}.
-
-Record retract_cond : Prop :=
-  {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}.
-
-
-(** The dependent elimination above implies the axiom of choice: *)
-Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
-Proof.
-intros r.
-case r; simpl.
-trivial.
-Qed.
-
-End Retracts.
-
-(** This lemma is basically a commutation of implication and existential
-    quantification:  (EX x | A -> P(x))  <=> (A -> EX x | P(x))
-    which is provable in classical logic ( => is already provable in
-    intuitionnistic logic). *)
-
-Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
-Proof.
-intros A B.
-destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf].
-  exists f0 g0; trivial.
-  exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros;
-    destruct hf; auto.
-Qed.
-
-
-(** The paradoxical set *)
-Definition U := forall P:Prop, pow P.
-
-(** Bijection between [U] and [(pow U)] *)
-Definition f (u:U) : pow U := u U.
-
-Definition g (h:pow U) : U :=
-  fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h).
-
-(** We deduce that the powerset of [U] is a retract of [U].
-    This lemma is stated in Berardi's article, but is not used
-    afterwards. *)
-Lemma retract_pow_U_U : retract (pow U) U.
-Proof.
-exists g f.
-intro a.
-unfold f, g; simpl.
-apply AC.
-exists (fun x:pow U => x) (fun x:pow U => x).
-trivial.
-Qed.
-
-(** Encoding of Russel's paradox *)
-
-(** The boolean negation. *)
-Definition Not_b (b:Bool) := IFProp (b = T) F T.
-
-(** the set of elements not belonging to itself *)
-Definition R : U := g (fun u:U => Not_b (u U u)).
-
-
-Lemma not_has_fixpoint : R R = Not_b (R R).
-Proof.
-unfold R at 1.
-unfold g.
-rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
-trivial.
-exists (fun x:pow U => x) (fun x:pow U => x); trivial.
-Qed.
-
-
-Theorem classical_proof_irrelevence : T = F.
-Proof.
-generalize not_has_fixpoint.
-unfold Not_b.
-apply AC_IF.
-intros is_true is_false.
-elim is_true; elim is_false; trivial.
-
-intros not_true is_true.
-elim not_true; trivial.
-Qed.
-
-End Berardis_paradox.
diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh
new file mode 100755
index 0000000000..1e2afb7540
--- /dev/null
+++ b/test-suite/misc/deps-checksum.sh
@@ -0,0 +1,5 @@
+rm -f misc/deps/*/*.vo
+$coqc -R misc/deps/A A misc/deps/A/A.v
+$coqc -R misc/deps/B A misc/deps/B/A.v
+$coqc -R misc/deps/B A misc/deps/B/B.v
+$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v
diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh
new file mode 100755
index 0000000000..375b706f0a
--- /dev/null
+++ b/test-suite/misc/deps-order.sh
@@ -0,0 +1,20 @@
+# Check that both coqdep and coqtop/coqc supports -R
+# Check that both coqdep and coqtop/coqc takes the later -R
+# See bugs 2242, 2337, 2339
+rm -f misc/deps/*/*.vo
+tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
+$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput
+diff -u misc/deps/deps.out $tmpoutput 2>&1
+R=$?
+times
+$coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1
+$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1
+$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1
+S=$?
+if [ $R = 0 -a $S = 0 ]; then
+    printf "coqdep and coqtop agree\n"
+    exit 0
+else
+    printf "coqdep and coqtop disagree\n"
+    exit 1
+fi
diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh
new file mode 100755
index 0000000000..cea1de862f
--- /dev/null
+++ b/test-suite/misc/exitstatus.sh
@@ -0,0 +1,7 @@
+$coqtop -load-vernac-source misc/exitstatus/illtyped.v
+N=$?
+$coqc misc/exitstatus/illtyped.v
+P=$?
+printf "On ill-typed input, coqtop returned $N.\n"
+printf "On ill-typed input, coqc returned $P.\n"
+if [ $N = 1 -a $P = 1 ]; then exit 0; else exit 1; fi
diff --git a/test-suite/misc/exitstatus/illtyped.v b/test-suite/misc/exitstatus/illtyped.v
new file mode 100644
index 0000000000..df6bbb389c
--- /dev/null
+++ b/test-suite/misc/exitstatus/illtyped.v
@@ -0,0 +1 @@
+Check S S.
diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh
new file mode 100755
index 0000000000..c822d0eb37
--- /dev/null
+++ b/test-suite/misc/printers.sh
@@ -0,0 +1,3 @@
+printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound
+if [ $? = 0 ]; then exit 1; else exit 0; fi
+
diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh
new file mode 100755
index 0000000000..d87a86035c
--- /dev/null
+++ b/test-suite/misc/universes.sh
@@ -0,0 +1,8 @@
+# Sort universes for the whole standard library
+EXPECTED_UNIVERSES=4 # Prop is not counted
+$coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1
+$coqc -R misc/universes Universes misc/universes/universes 2>&1
+mv universes.txt misc/universes
+N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l`
+printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES
+if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi