Imported Upstream version 8.3upstream/8.3

12 files changed, 165 insertions, 8 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 2503368f..62d443d0 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -40,6 +40,7 @@ endif
 
 command := $(coqtop) -top Top -load-vernac-source
 coqc := $(coqtop) -compile
+coqdep := $(BIN)coqdep
 
 SHOW := $(if $(VERBOSE),@true,@echo)
 HIDE := $(if $(VERBOSE),,@)
@@ -74,7 +75,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   interactive micromega $(COMPLEXITY) modules
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) xml bugs
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs
 
 #######################################################################
 # Phony targets
@@ -114,7 +115,6 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S))))
 # Summary
 #######################################################################
 
-summary_one = echo $(1); if [ -f $(2).log ]; then tail -n1 $(2).log; fi | sort -g
 summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 tail -q -n1 | sort -g
 
 .PHONY: summary summary.log
@@ -128,7 +128,7 @@ summary:
 	  $(call summary_dir, "Output tests", output); \
 	  $(call summary_dir, "Interactive tests", interactive); \
 	  $(call summary_dir, "Micromega tests", micromega); \
-	  $(call summary_one, "Miscellaneous tests", xml); \
+	  $(call summary_dir, "Miscellaneous tests", misc); \
 	  $(call summary_dir, "Complexity tests", complexity); \
 	  $(call summary_dir, "Module tests", modules); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
@@ -354,10 +354,12 @@ $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.
 # Miscellaneous tests
 #######################################################################
 
+misc: misc/xml.log misc/deps-order.log
+
 # Test xml compilation
-xml: xml.log
-xml.log:
-	@echo "TEST      xml"
+xml: misc/xml.log
+misc/xml.log:
+	@echo "TEST      misc/xml"
 	$(HIDE){ \
 	  echo $(call log_intro,xml); \
 	  rm -rf misc/xml; \
@@ -365,9 +367,36 @@ xml.log:
 	  $(bincoqc) -xml misc/berardi_test 2>&1; times; \
 	  if [ ! -d misc/xml ]; then \
 	    echo $(log_failure); \
-	    echo "    xml... failed"; \
+	    echo "    misc/xml... failed"; \
 	  else \
 	    echo $(log_success); \
-	    echo "    xml...apparently ok"; \
+	    echo "    misc/xml...apparently ok"; \
 	  fi; rm -r misc/xml; \
 	} > "$@"
+
+# Check that both coqdep and coqtop/coqc takes the later -I/-R
+# Check that both coqdep and coqtop/coqc supports both -R and -I dir -as lib
+# See bugs 2242, 2337, 2339
+deps-order: misc/deps-order.log
+misc/deps-order.log:
+	@echo "TEST      misc/deps-order"
+	$(HIDE){ \
+	  echo $(call log_intro,deps-order); \
+	  rm -f misc/deps/*/*.vo; \
+	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+	  $(coqdep) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \
+	    | head -n 1 > $$tmpoutput; \
+	  diff $$tmpoutput misc/deps/deps.out 2>&1; R=$$?; times; \
+	  $(bincoqc) -I misc/deps/lib -as lib misc/deps/lib/foo.v 2>&1; \
+	  $(bincoqc) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
+	  $(coqtop) -I misc/deps/lib -as lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \
+	  S=$$?; times; \
+	  if [ $$R = 0 -a $$S = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    misc/deps-order...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    misc/deps-order...Error! (unexpected order)"; \
+	  fi; \
+	  rm $$tmpoutput; \
+	} > "$@"
diff --git a/test-suite/bugs/closed/shouldsucceed/2360.v b/test-suite/bugs/closed/shouldsucceed/2360.v
new file mode 100644
index 00000000..4ae97c97
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2360.v
@@ -0,0 +1,13 @@
+(* This failed in V8.3 because descend_in_conjunctions built ill-typed terms *)
+Definition interp (etyp : nat -> Type) (p: nat) := etyp p.
+
+Record Value (etyp : nat -> Type) := Mk {
+  typ : nat; 
+  value : interp etyp typ
+}.
+
+Definition some_value (etyp : nat -> Type) :  (Value etyp).
+Proof.
+  intros.
+  Fail apply Mk. (* Check that it does not raise an anomaly *)
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2375.v b/test-suite/bugs/closed/shouldsucceed/2375.v
new file mode 100644
index 00000000..c17c426c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2375.v
@@ -0,0 +1,18 @@
+(* In the following code, the (superfluous) lemma [lem] is responsible 
+for the failure of congruence. *)
+
+Definition  f : nat -> Prop := fun x => True.
+
+Lemma lem : forall x,  (True -> True)   = ( True ->  f x).
+Proof.
+  intros. reflexivity.
+Qed.
+
+Goal forall  (x:nat), x = x.
+Proof.
+  intros.
+  assert (lem := lem).
+  (*clear ax.*)
+  congruence.
+Qed.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v
new file mode 100644
index 00000000..c7926711
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2388.v
@@ -0,0 +1,10 @@
+(* Error message was not printed in the correct environment *)
+
+Fail Parameters (A:Prop) (a:A A).
+
+(* This is a variant (reported as part of bug #2347) *)
+
+Require Import EquivDec.                                              
+Fail Program Instance bool_eq_eqdec : EqDec bool eq := 
+   {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
+
diff --git a/test-suite/failure/prop-set-proof-irrelevance.v b/test-suite/failure/prop-set-proof-irrelevance.v
new file mode 100644
index 00000000..ad494108
--- /dev/null
+++ b/test-suite/failure/prop-set-proof-irrelevance.v
@@ -0,0 +1,12 @@
+Require Import ProofIrrelevance.
+
+Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2.
+  exact proof_irrelevance.
+Qed.
+
+Lemma paradox : False.
+  assert (H : 0 <> 1) by discriminate.
+  apply H.
+  Fail apply proof_irrelevance. (* inlined version is rejected *)
+  apply proof_irrelevance_set.
+Qed.
diff --git a/test-suite/misc/deps/client/bar.v b/test-suite/misc/deps/client/bar.v
new file mode 100644
index 00000000..62969418
--- /dev/null
+++ b/test-suite/misc/deps/client/bar.v
@@ -0,0 +1,11 @@
+(* We assume the file compiled with -R ../lib lib -R . client *)
+(* foo alone should refer to client.foo because -R . client comes last *)
+
+Require Import foo.
+Goal a = 1.
+reflexivity.
+Qed.
+Require Import lib.foo.
+Goal a = 0.
+reflexivity.
+Qed.
diff --git a/test-suite/misc/deps/client/foo.v b/test-suite/misc/deps/client/foo.v
new file mode 100644
index 00000000..fc82069e
--- /dev/null
+++ b/test-suite/misc/deps/client/foo.v
@@ -0,0 +1 @@
+Definition a := 1.
diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out
new file mode 100644
index 00000000..68b48d60
--- /dev/null
+++ b/test-suite/misc/deps/deps.out
@@ -0,0 +1 @@
+misc/deps/client/bar.vo misc/deps/client/bar.glob: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo
diff --git a/test-suite/misc/deps/lib/foo.v b/test-suite/misc/deps/lib/foo.v
new file mode 100644
index 00000000..b745fbd4
--- /dev/null
+++ b/test-suite/misc/deps/lib/foo.v
@@ -0,0 +1 @@
+Definition a := 0.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 59e1a935..ce3e692f 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -86,3 +86,24 @@ Fixpoint plus n m {struct n} :=
   | 0 => m
   | S p => S (plus p m)
   end.
+
+(* Check multiple implicit arguments signatures *)
+
+Implicit Arguments eq_refl [[A] [x]] [[A]].
+
+Check eq_refl : 0 = 0.
+
+(* Check that notations preserve implicit (since 8.3) *)
+
+Parameter p : forall A, A -> forall n, n = 0 -> True.
+Implicit Arguments p [A n].
+Notation Q := (p 0).
+Check Q eq_refl.
+
+(* Check implicits with Context *)
+
+Section C.
+Context {A:Set}.
+Definition h (a:A) := a.
+End C.
+Check h 0.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index dfa41c82..02618c2c 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -243,3 +243,35 @@ test_open_match (forall z y, y + z  = 0).
 reflexivity.
 apply I.
 Qed.
+
+(* Test regular failure when clear/intro breaks soundness of the
+   interpretation of terms in current environment *)
+
+Ltac g y := clear y; assert (y=y).
+Goal forall x:nat, True.
+intro x.
+Fail g x.
+Abort.
+
+Ltac h y := assert (y=y).
+Goal forall x:nat, True.
+intro x.
+Fail clear x; f x.
+Abort.
+
+(* Do not consider evars as unification holes in Ltac matching (and at
+   least not as holes unrelated to the original evars)
+   [Example adapted from Ynot code]
+ *)
+
+Ltac not_eq e1 e2 :=
+  match e1 with
+    | e2 => fail 1
+    | _ => idtac
+  end.
+
+Goal True.
+evar(foo:nat).
+let evval := eval compute in foo in not_eq evval 1.
+let evval := eval compute in foo in not_eq 1 evval.
+Abort.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 47ca0836..5649e2f7 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -13,3 +13,11 @@ Goal EQ nat 0 0.
 Hint Unfold EQ.
 auto.
 Qed.
+
+(* Check regular failure when statically existing ref does not exist
+   any longer at run time *)
+
+Goal let x := 0 in True.
+intro x.
+Fail (clear x; unfold x).
+Abort.