diff options
Diffstat (limited to 'test-suite')
45 files changed, 664 insertions, 322 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index f7447d6cec..5d4e15b985 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -198,7 +198,6 @@ summary: $(call summary_dir, "Coqdoc tests", coqdoc); \ $(call summary_dir, "tools/ tests", tools); \ $(call summary_dir, "Unit tests", unit-tests); \ - $(call summary_dir, "Machine arithmetic tests", arithmetic); \ $(call summary_dir, "Ltac2 tests", ltac2); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ @@ -223,7 +222,7 @@ report: summary.log # printed for all opened bugs (still active or seems to be closed). # For closed bugs that behave as expected, no message is printed -# All files are assumed to have <# of the bug>.v as a name +# All files are assumed to have bug_<# of the bug>.v as a name # Opened bugs that should not fail $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v @@ -501,8 +500,8 @@ $(addsuffix .log,$(wildcard output-coqchk/*.v)): %.v.log: %.v %.out $(PREREQUISI } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi .PHONY: approve-output -approve-output: output output-coqtop - $(HIDE)for f in output/*.out.real; do \ +approve-output: output output-coqtop output-coqchk + $(HIDE)for f in $(wildcard $(addsuffix /*.out.real,$^)); do \ mv "$$f" "$${f%.real}"; \ echo "Updated $${f%.real}!"; \ done diff --git a/test-suite/bugs/bug_5996.v b/test-suite/bugs/bug_5996.v deleted file mode 100644 index c9e3292b48..0000000000 --- a/test-suite/bugs/bug_5996.v +++ /dev/null @@ -1,8 +0,0 @@ -Goal Type. - let c := constr:(prod nat nat) in - let c' := (eval pattern nat in c) in - let c' := lazymatch c' with ?f _ => f end in - let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in - let _ := type of c'' in - exact c''. -Defined. diff --git a/test-suite/bugs/bug_11140.v b/test-suite/bugs/closed/bug_11140.v index ca806ea324..ca806ea324 100644 --- a/test-suite/bugs/bug_11140.v +++ b/test-suite/bugs/closed/bug_11140.v diff --git a/test-suite/bugs/closed/bug_12001.v b/test-suite/bugs/closed/bug_12001.v new file mode 100644 index 0000000000..19533e49f1 --- /dev/null +++ b/test-suite/bugs/closed/bug_12001.v @@ -0,0 +1,24 @@ +(* Argument names don't get mangled *) +Set Mangle Names. +Lemma leibniz_equiv_iff {A : Type} (x y : A) : True. +Proof. tauto. Qed. +Check leibniz_equiv_iff (A := nat) 2 3 : True. +Unset Mangle Names. + +(* Coq doesn't make up names for arguments *) +Definition bar (a a : nat) : nat := 3. +Arguments bar _ _ : assert. +Fail Arguments bar a a0 : assert. + +(* This definition caused an anomaly in a version of this PR +without the change to prepare_implicits *) +Set Implicit Arguments. +Definition foo (_ : nat) (_ : @eq nat ltac:(assumption) 2) : True := I. +Fail Check foo (H := 2). + +Definition baz (a b : nat) := b. +Arguments baz a {b}. +Set Mangle Names. +Definition baz2 (a b : nat) := b. +Arguments baz2 a {b}. +Unset Mangle Names. diff --git a/test-suite/bugs/closed/bug_12483.v b/test-suite/bugs/closed/bug_12483.v index 0d034a65eb..ae46117e59 100644 --- a/test-suite/bugs/closed/bug_12483.v +++ b/test-suite/bugs/closed/bug_12483.v @@ -4,7 +4,7 @@ Goal False. Proof. cut (false = true). { intro H; discriminate H. } -change false with (1 <= 0)%float. +change false with (1 <=? 0)%float. rewrite leb_spec. Fail reflexivity. Abort. diff --git a/test-suite/bugs/closed/bug_12763.v b/test-suite/bugs/closed/bug_12763.v new file mode 100644 index 0000000000..6cbcc0d3b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_12763.v @@ -0,0 +1,6 @@ +Inductive bool_list := S (y : bool) (l : bool_list) | O. +Scheme Equality for bool_list. + +Set Mangle Names. +Scheme Equality for nat. +Scheme Equality for list. diff --git a/test-suite/bugs/closed/bug_12787.v b/test-suite/bugs/closed/bug_12787.v new file mode 100644 index 0000000000..2566e1f261 --- /dev/null +++ b/test-suite/bugs/closed/bug_12787.v @@ -0,0 +1,26 @@ +Inductive sigT3 {A: Type} {P: A -> Type} (Q: forall a: A, P a -> Type) := + existT3: forall a: A, forall b: P a, Q a b -> sigT3 Q +. + +Definition projT3_1 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) := + let 'existT3 _ x0 _ _ := a in x0. + +Definition projT3_2 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) : P (projT3_1 a) := + let 'existT3 _ x0 x1 _ := a in x1. + + + +Lemma projT3_3_eq' (A B: Type) (Q: B -> Type) (a b: sigT3 (fun (_: A) b => Q b)) (H: a = b) : + unit. +Proof. + destruct a as [x0 x1 x2], b as [y0 y1 y2]. + assert (H' := f_equal projT3_1 H). + cbn in H'. + subst x0. + assert (H' := f_equal (projT3_2 (P := fun _ => B)) H). + cbn in H'. + subst x1. + + injection H as H'. + exact tt. +Qed. diff --git a/test-suite/bugs/bug_4690.v b/test-suite/bugs/closed/bug_4690.v index f50866a990..f50866a990 100644 --- a/test-suite/bugs/bug_4690.v +++ b/test-suite/bugs/closed/bug_4690.v diff --git a/test-suite/bugs/closed/bug_7015.v b/test-suite/bugs/closed/bug_7015.v new file mode 100644 index 0000000000..a57fa94960 --- /dev/null +++ b/test-suite/bugs/closed/bug_7015.v @@ -0,0 +1,74 @@ +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. +Set Printing Universes. + +Module Simple. + + (* in the real world foo@{i} might be [@paths@{i} nat] I guess *) + Inductive foo : nat -> Type :=. + + (* on [refl (fun x => f x)] this computes to [refl f] *) + Definition eta_out {A B} (f g : forall x : A, B x) (e : (fun x => f x) = (fun x => g x)) : f = g. + Proof. + change (f = g) in e. destruct e;reflexivity. + Defined. + + Section univs. + Universes i j. + Constraint i < j. (* fail instead of forcing equality *) + + Definition one : (fun n => foo@{i} n) = fun n => foo@{j} n := eq_refl. + + Definition two : foo@{i} = foo@{j} := eta_out _ _ one. + + Definition two' : foo@{i} = foo@{j} := Eval compute in two. + + Definition three := @eq_refl (foo@{i} = foo@{j}) two. + Definition four := Eval compute in three. + + Definition five : foo@{i} = foo@{j} := eq_refl. + End univs. + + (* inference tries and succeeds with syntactic equality which doesn't eta expand *) + Fail Definition infer@{i j k|i < k, j < k, k < eq.u0} + : foo@{i} = foo@{j} :> (nat -> Type@{k}) + := eq_refl. + +End Simple. + +Module WithRed. + (** this test needs to reduce the parameter's type to work *) + + + Inductive foo@{i j} (b:bool) (x:if b return Type@{j} then Type@{i} else nat) : Type@{i} := . + + (* on [refl (fun x => f x)] this computes to [refl f] *) + Definition eta_out {A B} (f g : forall x : A, B x) (e : (fun x => f x) = (fun x => g x)) : f = g. + Proof. + change (f = g) in e. destruct e;reflexivity. + Defined. + + Section univs. + Universes i j k. + Constraint i < j. (* fail instead of forcing equality *) + + Definition one : (fun n => foo@{i k} false n) = fun n => foo@{j k} false n := eq_refl. + + Definition two : foo@{i k} false = foo@{j k} false := eta_out _ _ one. + + Definition two' : foo@{i k} false = foo@{j k} false := Eval compute in two. + + (* Failure of SR doesn't just mean that the type changes, sometimes + we lose being well-typed entirely. *) + Definition three := @eq_refl (foo@{i k} false = foo@{j k} false) two. + Definition four := Eval compute in three. + + Definition five : foo@{i k} false = foo@{j k} false := eq_refl. + End univs. + + (* inference tries and succeeds with syntactic equality which doesn't eta expand *) + Fail Definition infer@{i j k|i < k, j < k, k < eq.u0} + : foo@{i k} false = foo@{j k} false :> (nat -> Type@{k}) + := eq_refl. + +End WithRed. diff --git a/test-suite/bugs/bug_9490.v b/test-suite/bugs/closed/bug_9490.v index a5def40c49..a5def40c49 100644 --- a/test-suite/bugs/bug_9490.v +++ b/test-suite/bugs/closed/bug_9490.v diff --git a/test-suite/bugs/bug_9532.v b/test-suite/bugs/closed/bug_9532.v index d198d45f2f..d198d45f2f 100644 --- a/test-suite/bugs/bug_9532.v +++ b/test-suite/bugs/closed/bug_9532.v diff --git a/test-suite/bugs/opened/bug_2904.v b/test-suite/bugs/opened/bug_2904.v new file mode 100644 index 0000000000..da30a509ac --- /dev/null +++ b/test-suite/bugs/opened/bug_2904.v @@ -0,0 +1,18 @@ +Module Type S. +Parameter t : Type. +Module M'. +Parameter t : Type. +Definition u := S.t. +End M'. +End S. + +Module M : S. +Definition t := unit. +Module M'. +Definition t := bool. +Definition u := M.t. +End M'. +End M. + +Require Extraction. +Fail Extraction TestCompile M. diff --git a/test-suite/bugs/opened/bug_5996.v b/test-suite/bugs/opened/bug_5996.v new file mode 100644 index 0000000000..2e81a183cd --- /dev/null +++ b/test-suite/bugs/opened/bug_5996.v @@ -0,0 +1,19 @@ +(* Original example *) +Goal Type. + let c := constr:(prod nat nat) in + let c' := (eval pattern nat in c) in + let c' := lazymatch c' with ?f _ => f end in + let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in + exact c''. +Fail Defined. +Abort. + +(* Workaround *) +Goal Type. + let c := constr:(prod nat nat) in + let c' := (eval pattern nat in c) in + let c' := lazymatch c' with ?f _ => f end in + let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in + let _ := type of c'' in + exact c''. +Defined. diff --git a/test-suite/coqdoc/details.html.out b/test-suite/coqdoc/details.html.out new file mode 100644 index 0000000000..e1f1ad9867 --- /dev/null +++ b/test-suite/coqdoc/details.html.out @@ -0,0 +1,48 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.details</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.details</h1> + +<div class="code"> +</div> +<details><div class="code"> +<span class="id" title="keyword">Definition</span> <a id="foo" class="idref" href="#foo"><span class="id" title="definition">foo</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := 3.<br/> +</div> +</details><div class="code"> + +<br/> +</div> +<details><summary>Foo bar </summary><div class="code"> +<span class="id" title="keyword">Fixpoint</span> <a id="idnat" class="idref" href="#idnat"><span class="id" title="definition">idnat</span></a> (<a id="x:1" class="idref" href="#x:1"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/> + <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> + | <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="Coqdoc.details.html#idnat:2"><span class="id" title="definition">idnat</span></a> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a>)<br/> + | 0 ⇒ 0<br/> + <span class="id" title="keyword">end</span>.<br/> +</div> +</details><div class="code"> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/details.tex.out b/test-suite/coqdoc/details.tex.out new file mode 100644 index 0000000000..37778944ba --- /dev/null +++ b/test-suite/coqdoc/details.tex.out @@ -0,0 +1,44 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.details}{Library }{Coqdoc.details} + +\begin{coqdoccode} +\end{coqdoccode} +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.details.foo}{foo}{\coqdocdefinition{foo}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} := 3.\coqdoceol +\end{coqdoccode} +\begin{coqdoccode} +\coqdocemptyline +\end{coqdoccode} +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Fixpoint} \coqdef{Coqdoc.details.idnat}{idnat}{\coqdocdefinition{idnat}} (\coqdef{Coqdoc.details.x:1}{x}{\coqdocbinder{x}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} :=\coqdoceol +\coqdocindent{1.00em} +\coqdockw{match} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} \coqdocvar{x} \ensuremath{\Rightarrow} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} (\coqref{Coqdoc.details.idnat:2}{\coqdocdefinition{idnat}} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}})\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} 0 \ensuremath{\Rightarrow} 0\coqdoceol +\coqdocindent{1.00em} +\coqdockw{end}.\coqdoceol +\end{coqdoccode} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/details.v b/test-suite/coqdoc/details.v new file mode 100644 index 0000000000..208e60317d --- /dev/null +++ b/test-suite/coqdoc/details.v @@ -0,0 +1,11 @@ +(* begin details *) +Definition foo : nat := 3. +(* end details *) + +(* begin details : Foo bar *) +Fixpoint idnat (x : nat) : nat := + match x with + | S x => S (idnat x) + | 0 => 0 + end. +(* end details *) diff --git a/test-suite/micromega/bug_12790.v b/test-suite/micromega/bug_12790.v new file mode 100644 index 0000000000..39d640ebd9 --- /dev/null +++ b/test-suite/micromega/bug_12790.v @@ -0,0 +1,8 @@ +Require Import Lia. + +Goal forall (a b c d x: nat), +S c = a - b -> x <= x + (S c) * d. +Proof. +intros a b c d x H. +lia. +Qed. diff --git a/test-suite/micromega/bug_12791.v b/test-suite/micromega/bug_12791.v new file mode 100644 index 0000000000..8aec1904a4 --- /dev/null +++ b/test-suite/micromega/bug_12791.v @@ -0,0 +1,9 @@ +Require Import Lia. + +Definition t := nat. + +Goal forall (a b: t), let c := a in b = a -> b = c. +Proof. + intros a b c H. + lia. +Qed. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e0aa758812..c28bb14eb3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -84,8 +84,6 @@ Argument lists should agree on the names they provide. The command has indeed failed with message: Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Some argument names are duplicated: F -The command has indeed failed with message: Argument number 3 is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 6ac09cf771..6001850046 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -48,7 +48,6 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. -Fail Arguments eq_refl {F F}, [F] F : rename. Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. diff --git a/test-suite/output/ErrorLocation_12774_1.out b/test-suite/output/ErrorLocation_12774_1.out new file mode 100644 index 0000000000..e27992ed59 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_1.out @@ -0,0 +1,3 @@ +File "stdin", line 2, characters 13-14: +Error: The term "0" has type "nat" while it is expected to have type "Type". + diff --git a/test-suite/output/ErrorLocation_12774_1.v b/test-suite/output/ErrorLocation_12774_1.v new file mode 100644 index 0000000000..8516d402d1 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_1.v @@ -0,0 +1,3 @@ +Goal Type. +simpl; exact 0. +Abort. diff --git a/test-suite/output/ErrorLocation_12774_2.out b/test-suite/output/ErrorLocation_12774_2.out new file mode 100644 index 0000000000..434275eca5 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_2.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 9-10: +Error: The term "0" has type "nat" while it is expected to have type "Type". + diff --git a/test-suite/output/ErrorLocation_12774_2.v b/test-suite/output/ErrorLocation_12774_2.v new file mode 100644 index 0000000000..e50e1caa0f --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_2.v @@ -0,0 +1,4 @@ +Ltac f := simpl. +Goal Type. +f; exact 0. +Abort. diff --git a/test-suite/output/ErrorLocation_12774_3.out b/test-suite/output/ErrorLocation_12774_3.out new file mode 100644 index 0000000000..dbd3dbd1e2 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-1: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12774_3.v b/test-suite/output/ErrorLocation_12774_3.v new file mode 100644 index 0000000000..c624402a81 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.v @@ -0,0 +1,4 @@ +Ltac f := auto; intro. +Goal False. +f. +Abort. diff --git a/test-suite/output/ErrorLocation_tac_in_term_1.out b/test-suite/output/ErrorLocation_tac_in_term_1.out new file mode 100644 index 0000000000..55ad5a36da --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_1.out @@ -0,0 +1,4 @@ +File "stdin", line 2, characters 21-25: +Error: +The term "true" has type "bool" while it is expected to have type "nat". + diff --git a/test-suite/output/ErrorLocation_tac_in_term_1.v b/test-suite/output/ErrorLocation_tac_in_term_1.v new file mode 100644 index 0000000000..ef0b5aa757 --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_1.v @@ -0,0 +1,3 @@ +Goal True. +apply ltac:(apply (S true)). +Abort. diff --git a/test-suite/output/ErrorLocation_tac_in_term_2.out b/test-suite/output/ErrorLocation_tac_in_term_2.out new file mode 100644 index 0000000000..5bff5ede43 --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_2.out @@ -0,0 +1,4 @@ +File "stdin", line 4, characters 12-20: +Error: +The term "true" has type "bool" while it is expected to have type "nat". + diff --git a/test-suite/output/ErrorLocation_tac_in_term_2.v b/test-suite/output/ErrorLocation_tac_in_term_2.v new file mode 100644 index 0000000000..e0fc2a9f4f --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_2.v @@ -0,0 +1,5 @@ +Ltac f x y := apply (x y). + +Goal True. +apply ltac:(f S true). +Abort. diff --git a/test-suite/output/Error_msg_diffs.out b/test-suite/output/Error_msg_diffs.out index 3e337e892d..2645524a70 100644 --- a/test-suite/output/Error_msg_diffs.out +++ b/test-suite/output/Error_msg_diffs.out @@ -1,4 +1,4 @@ -File "stdin", line 32, characters 0-12: +File "stdin", line 32, characters 0-11: [37;41;1mError:[0m In environment T : [33;1mType[0m diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index ef7667936c..2265028d3e 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments d2 [x x0]%nat_scope +Arguments d2 [x x]%nat_scope map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out index 7c80a6065f..28beee90b2 100644 --- a/test-suite/output/RecordMissingField.out +++ b/test-suite/output/RecordMissingField.out @@ -1,4 +1,16 @@ -File "stdin", line 8, characters 5-22: -Error: Cannot infer field y2p of record point2d in environment: -p : point2d - +The command has indeed failed with message: +The following term contains unresolved implicit arguments: + (fun p : point2d => {| x2p := x2p p + 1; y2p := ?y2p |}) +More precisely: +- ?y2p: Cannot infer field y2p of record point2d in environment: + p : point2d +The command has indeed failed with message: +The following term contains unresolved implicit arguments: + (fun p : point2d => {| x2p := x2p p + (fun n : nat => ?n) 1; y2p := ?y2p |}) +More precisely: +- ?n: Cannot infer this placeholder of type "nat" in + environment: + p : point2d + n : nat +- ?y2p: Cannot infer field y2p of record point2d in environment: + p : point2d diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v index 84f1748fa0..8ca721564b 100644 --- a/test-suite/output/RecordMissingField.v +++ b/test-suite/output/RecordMissingField.v @@ -3,6 +3,10 @@ should contain missing field, and the inferred type of the record **) Record point2d := mkPoint { x2p: nat; y2p: nat }. - -Definition increment_x (p: point2d) : point2d := +Fail Definition increment_x (p: point2d) : point2d := {| x2p := x2p p + 1; |}. + +(* Here there is also an unresolved implicit, which should give an + understadable error as well *) +Fail Definition increment_x (p: point2d) : point2d := + {| x2p := x2p p + (fun n => _) 1; |}. diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.out b/test-suite/output/ssr_error_multiple_intro_after_case.out new file mode 100644 index 0000000000..51fb208ae9 --- /dev/null +++ b/test-suite/output/ssr_error_multiple_intro_after_case.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-11: +Error: x already used + diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v new file mode 100644 index 0000000000..1f87966693 --- /dev/null +++ b/test-suite/output/ssr_error_multiple_intro_after_case.v @@ -0,0 +1,3 @@ +Require Import ssreflect. +Goal forall p : nat * nat , True. +case => x x. diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v index 23d1e5bbae..75fd5c426f 100644 --- a/test-suite/primitive/float/compare.v +++ b/test-suite/primitive/float/compare.v @@ -6,380 +6,380 @@ Definition min_denorm := Eval compute in ldexp one (-1074)%Z. Definition min_norm := Eval compute in ldexp one (-1024)%Z. -Check (eq_refl false : nan == nan = false). -Check (eq_refl false : nan == nan = false). -Check (eq_refl false : nan < nan = false). -Check (eq_refl false : nan < nan = false). -Check (eq_refl false : nan <= nan = false). -Check (eq_refl false : nan <= nan = false). +Check (eq_refl false : nan =? nan = false). +Check (eq_refl false : nan =? nan = false). +Check (eq_refl false : nan <? nan = false). +Check (eq_refl false : nan <? nan = false). +Check (eq_refl false : nan <=? nan = false). +Check (eq_refl false : nan <=? nan = false). Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). -Check (eq_refl false <: nan == nan = false). -Check (eq_refl false <: nan == nan = false). -Check (eq_refl false <: nan < nan = false). -Check (eq_refl false <: nan < nan = false). -Check (eq_refl false <: nan <= nan = false). -Check (eq_refl false <: nan <= nan = false). +Check (eq_refl false <: nan =? nan = false). +Check (eq_refl false <: nan =? nan = false). +Check (eq_refl false <: nan <? nan = false). +Check (eq_refl false <: nan <? nan = false). +Check (eq_refl false <: nan <=? nan = false). +Check (eq_refl false <: nan <=? nan = false). Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). -Check (eq_refl false <<: nan == nan = false). -Check (eq_refl false <<: nan == nan = false). -Check (eq_refl false <<: nan < nan = false). -Check (eq_refl false <<: nan < nan = false). -Check (eq_refl false <<: nan <= nan = false). -Check (eq_refl false <<: nan <= nan = false). +Check (eq_refl false <<: nan =? nan = false). +Check (eq_refl false <<: nan =? nan = false). +Check (eq_refl false <<: nan <? nan = false). +Check (eq_refl false <<: nan <? nan = false). +Check (eq_refl false <<: nan <=? nan = false). +Check (eq_refl false <<: nan <=? nan = false). Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). -Check (eq_refl false : nan == - nan = false). -Check (eq_refl false : - nan == nan = false). -Check (eq_refl false : nan < - nan = false). -Check (eq_refl false : - nan < nan = false). -Check (eq_refl false : nan <= - nan = false). -Check (eq_refl false : - nan <= nan = false). +Check (eq_refl false : nan =? - nan = false). +Check (eq_refl false : - nan =? nan = false). +Check (eq_refl false : nan <? - nan = false). +Check (eq_refl false : - nan <? nan = false). +Check (eq_refl false : nan <=? - nan = false). +Check (eq_refl false : - nan <=? nan = false). Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable). Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable). -Check (eq_refl false <: nan == - nan = false). -Check (eq_refl false <: - nan == nan = false). -Check (eq_refl false <: nan < - nan = false). -Check (eq_refl false <: - nan < nan = false). -Check (eq_refl false <: nan <= - nan = false). -Check (eq_refl false <: - nan <= nan = false). +Check (eq_refl false <: nan =? - nan = false). +Check (eq_refl false <: - nan =? nan = false). +Check (eq_refl false <: nan <? - nan = false). +Check (eq_refl false <: - nan <? nan = false). +Check (eq_refl false <: nan <=? - nan = false). +Check (eq_refl false <: - nan <=? nan = false). Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable). Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable). -Check (eq_refl false <<: nan == - nan = false). -Check (eq_refl false <<: - nan == nan = false). -Check (eq_refl false <<: nan < - nan = false). -Check (eq_refl false <<: - nan < nan = false). -Check (eq_refl false <<: nan <= - nan = false). -Check (eq_refl false <<: - nan <= nan = false). +Check (eq_refl false <<: nan =? - nan = false). +Check (eq_refl false <<: - nan =? nan = false). +Check (eq_refl false <<: nan <? - nan = false). +Check (eq_refl false <<: - nan <? nan = false). +Check (eq_refl false <<: nan <=? - nan = false). +Check (eq_refl false <<: - nan <=? nan = false). Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable). Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable). -Check (eq_refl true : one == one = true). -Check (eq_refl true : one == one = true). -Check (eq_refl false : one < one = false). -Check (eq_refl false : one < one = false). -Check (eq_refl true : one <= one = true). -Check (eq_refl true : one <= one = true). +Check (eq_refl true : one =? one = true). +Check (eq_refl true : one =? one = true). +Check (eq_refl false : one <? one = false). +Check (eq_refl false : one <? one = false). +Check (eq_refl true : one <=? one = true). +Check (eq_refl true : one <=? one = true). Check (eq_refl FEq : one ?= one = FEq). Check (eq_refl FEq : one ?= one = FEq). -Check (eq_refl true <: one == one = true). -Check (eq_refl true <: one == one = true). -Check (eq_refl false <: one < one = false). -Check (eq_refl false <: one < one = false). -Check (eq_refl true <: one <= one = true). -Check (eq_refl true <: one <= one = true). +Check (eq_refl true <: one =? one = true). +Check (eq_refl true <: one =? one = true). +Check (eq_refl false <: one <? one = false). +Check (eq_refl false <: one <? one = false). +Check (eq_refl true <: one <=? one = true). +Check (eq_refl true <: one <=? one = true). Check (eq_refl FEq <: one ?= one = FEq). Check (eq_refl FEq <: one ?= one = FEq). -Check (eq_refl true <<: one == one = true). -Check (eq_refl true <<: one == one = true). -Check (eq_refl false <<: one < one = false). -Check (eq_refl false <<: one < one = false). -Check (eq_refl true <<: one <= one = true). -Check (eq_refl true <<: one <= one = true). +Check (eq_refl true <<: one =? one = true). +Check (eq_refl true <<: one =? one = true). +Check (eq_refl false <<: one <? one = false). +Check (eq_refl false <<: one <? one = false). +Check (eq_refl true <<: one <=? one = true). +Check (eq_refl true <<: one <=? one = true). Check (eq_refl FEq <<: one ?= one = FEq). Check (eq_refl FEq <<: one ?= one = FEq). -Check (eq_refl true : zero == zero = true). -Check (eq_refl true : zero == zero = true). -Check (eq_refl false : zero < zero = false). -Check (eq_refl false : zero < zero = false). -Check (eq_refl true : zero <= zero = true). -Check (eq_refl true : zero <= zero = true). +Check (eq_refl true : zero =? zero = true). +Check (eq_refl true : zero =? zero = true). +Check (eq_refl false : zero <? zero = false). +Check (eq_refl false : zero <? zero = false). +Check (eq_refl true : zero <=? zero = true). +Check (eq_refl true : zero <=? zero = true). Check (eq_refl FEq : zero ?= zero = FEq). Check (eq_refl FEq : zero ?= zero = FEq). -Check (eq_refl true <: zero == zero = true). -Check (eq_refl true <: zero == zero = true). -Check (eq_refl false <: zero < zero = false). -Check (eq_refl false <: zero < zero = false). -Check (eq_refl true <: zero <= zero = true). -Check (eq_refl true <: zero <= zero = true). +Check (eq_refl true <: zero =? zero = true). +Check (eq_refl true <: zero =? zero = true). +Check (eq_refl false <: zero <? zero = false). +Check (eq_refl false <: zero <? zero = false). +Check (eq_refl true <: zero <=? zero = true). +Check (eq_refl true <: zero <=? zero = true). Check (eq_refl FEq <: zero ?= zero = FEq). Check (eq_refl FEq <: zero ?= zero = FEq). -Check (eq_refl true <<: zero == zero = true). -Check (eq_refl true <<: zero == zero = true). -Check (eq_refl false <<: zero < zero = false). -Check (eq_refl false <<: zero < zero = false). -Check (eq_refl true <<: zero <= zero = true). -Check (eq_refl true <<: zero <= zero = true). +Check (eq_refl true <<: zero =? zero = true). +Check (eq_refl true <<: zero =? zero = true). +Check (eq_refl false <<: zero <? zero = false). +Check (eq_refl false <<: zero <? zero = false). +Check (eq_refl true <<: zero <=? zero = true). +Check (eq_refl true <<: zero <=? zero = true). Check (eq_refl FEq <<: zero ?= zero = FEq). Check (eq_refl FEq <<: zero ?= zero = FEq). -Check (eq_refl true : zero == - zero = true). -Check (eq_refl true : - zero == zero = true). -Check (eq_refl false : zero < - zero = false). -Check (eq_refl false : - zero < zero = false). -Check (eq_refl true : zero <= - zero = true). -Check (eq_refl true : - zero <= zero = true). +Check (eq_refl true : zero =? - zero = true). +Check (eq_refl true : - zero =? zero = true). +Check (eq_refl false : zero <? - zero = false). +Check (eq_refl false : - zero <? zero = false). +Check (eq_refl true : zero <=? - zero = true). +Check (eq_refl true : - zero <=? zero = true). Check (eq_refl FEq : zero ?= - zero = FEq). Check (eq_refl FEq : - zero ?= zero = FEq). -Check (eq_refl true <: zero == - zero = true). -Check (eq_refl true <: - zero == zero = true). -Check (eq_refl false <: zero < - zero = false). -Check (eq_refl false <: - zero < zero = false). -Check (eq_refl true <: zero <= - zero = true). -Check (eq_refl true <: - zero <= zero = true). +Check (eq_refl true <: zero =? - zero = true). +Check (eq_refl true <: - zero =? zero = true). +Check (eq_refl false <: zero <? - zero = false). +Check (eq_refl false <: - zero <? zero = false). +Check (eq_refl true <: zero <=? - zero = true). +Check (eq_refl true <: - zero <=? zero = true). Check (eq_refl FEq <: zero ?= - zero = FEq). Check (eq_refl FEq <: - zero ?= zero = FEq). -Check (eq_refl true <<: zero == - zero = true). -Check (eq_refl true <<: - zero == zero = true). -Check (eq_refl false <<: zero < - zero = false). -Check (eq_refl false <<: - zero < zero = false). -Check (eq_refl true <<: zero <= - zero = true). -Check (eq_refl true <<: - zero <= zero = true). +Check (eq_refl true <<: zero =? - zero = true). +Check (eq_refl true <<: - zero =? zero = true). +Check (eq_refl false <<: zero <? - zero = false). +Check (eq_refl false <<: - zero <? zero = false). +Check (eq_refl true <<: zero <=? - zero = true). +Check (eq_refl true <<: - zero <=? zero = true). Check (eq_refl FEq <<: zero ?= - zero = FEq). Check (eq_refl FEq <<: - zero ?= zero = FEq). -Check (eq_refl true : - zero == - zero = true). -Check (eq_refl true : - zero == - zero = true). -Check (eq_refl false : - zero < - zero = false). -Check (eq_refl false : - zero < - zero = false). -Check (eq_refl true : - zero <= - zero = true). -Check (eq_refl true : - zero <= - zero = true). +Check (eq_refl true : - zero =? - zero = true). +Check (eq_refl true : - zero =? - zero = true). +Check (eq_refl false : - zero <? - zero = false). +Check (eq_refl false : - zero <? - zero = false). +Check (eq_refl true : - zero <=? - zero = true). +Check (eq_refl true : - zero <=? - zero = true). Check (eq_refl FEq : - zero ?= - zero = FEq). Check (eq_refl FEq : - zero ?= - zero = FEq). -Check (eq_refl true <: - zero == - zero = true). -Check (eq_refl true <: - zero == - zero = true). -Check (eq_refl false <: - zero < - zero = false). -Check (eq_refl false <: - zero < - zero = false). -Check (eq_refl true <: - zero <= - zero = true). -Check (eq_refl true <: - zero <= - zero = true). +Check (eq_refl true <: - zero =? - zero = true). +Check (eq_refl true <: - zero =? - zero = true). +Check (eq_refl false <: - zero <? - zero = false). +Check (eq_refl false <: - zero <? - zero = false). +Check (eq_refl true <: - zero <=? - zero = true). +Check (eq_refl true <: - zero <=? - zero = true). Check (eq_refl FEq <: - zero ?= - zero = FEq). Check (eq_refl FEq <: - zero ?= - zero = FEq). -Check (eq_refl true <<: - zero == - zero = true). -Check (eq_refl true <<: - zero == - zero = true). -Check (eq_refl false <<: - zero < - zero = false). -Check (eq_refl false <<: - zero < - zero = false). -Check (eq_refl true <<: - zero <= - zero = true). -Check (eq_refl true <<: - zero <= - zero = true). +Check (eq_refl true <<: - zero =? - zero = true). +Check (eq_refl true <<: - zero =? - zero = true). +Check (eq_refl false <<: - zero <? - zero = false). +Check (eq_refl false <<: - zero <? - zero = false). +Check (eq_refl true <<: - zero <=? - zero = true). +Check (eq_refl true <<: - zero <=? - zero = true). Check (eq_refl FEq <<: - zero ?= - zero = FEq). Check (eq_refl FEq <<: - zero ?= - zero = FEq). -Check (eq_refl true : infinity == infinity = true). -Check (eq_refl true : infinity == infinity = true). -Check (eq_refl false : infinity < infinity = false). -Check (eq_refl false : infinity < infinity = false). -Check (eq_refl true : infinity <= infinity = true). -Check (eq_refl true : infinity <= infinity = true). +Check (eq_refl true : infinity =? infinity = true). +Check (eq_refl true : infinity =? infinity = true). +Check (eq_refl false : infinity <? infinity = false). +Check (eq_refl false : infinity <? infinity = false). +Check (eq_refl true : infinity <=? infinity = true). +Check (eq_refl true : infinity <=? infinity = true). Check (eq_refl FEq : infinity ?= infinity = FEq). Check (eq_refl FEq : infinity ?= infinity = FEq). -Check (eq_refl true <: infinity == infinity = true). -Check (eq_refl true <: infinity == infinity = true). -Check (eq_refl false <: infinity < infinity = false). -Check (eq_refl false <: infinity < infinity = false). -Check (eq_refl true <: infinity <= infinity = true). -Check (eq_refl true <: infinity <= infinity = true). +Check (eq_refl true <: infinity =? infinity = true). +Check (eq_refl true <: infinity =? infinity = true). +Check (eq_refl false <: infinity <? infinity = false). +Check (eq_refl false <: infinity <? infinity = false). +Check (eq_refl true <: infinity <=? infinity = true). +Check (eq_refl true <: infinity <=? infinity = true). Check (eq_refl FEq <: infinity ?= infinity = FEq). Check (eq_refl FEq <: infinity ?= infinity = FEq). -Check (eq_refl true <<: infinity == infinity = true). -Check (eq_refl true <<: infinity == infinity = true). -Check (eq_refl false <<: infinity < infinity = false). -Check (eq_refl false <<: infinity < infinity = false). -Check (eq_refl true <<: infinity <= infinity = true). -Check (eq_refl true <<: infinity <= infinity = true). +Check (eq_refl true <<: infinity =? infinity = true). +Check (eq_refl true <<: infinity =? infinity = true). +Check (eq_refl false <<: infinity <? infinity = false). +Check (eq_refl false <<: infinity <? infinity = false). +Check (eq_refl true <<: infinity <=? infinity = true). +Check (eq_refl true <<: infinity <=? infinity = true). Check (eq_refl FEq <<: infinity ?= infinity = FEq). Check (eq_refl FEq <<: infinity ?= infinity = FEq). -Check (eq_refl true : - infinity == - infinity = true). -Check (eq_refl true : - infinity == - infinity = true). -Check (eq_refl false : - infinity < - infinity = false). -Check (eq_refl false : - infinity < - infinity = false). -Check (eq_refl true : - infinity <= - infinity = true). -Check (eq_refl true : - infinity <= - infinity = true). +Check (eq_refl true : - infinity =? - infinity = true). +Check (eq_refl true : - infinity =? - infinity = true). +Check (eq_refl false : - infinity <? - infinity = false). +Check (eq_refl false : - infinity <? - infinity = false). +Check (eq_refl true : - infinity <=? - infinity = true). +Check (eq_refl true : - infinity <=? - infinity = true). Check (eq_refl FEq : - infinity ?= - infinity = FEq). Check (eq_refl FEq : - infinity ?= - infinity = FEq). -Check (eq_refl true <: - infinity == - infinity = true). -Check (eq_refl true <: - infinity == - infinity = true). -Check (eq_refl false <: - infinity < - infinity = false). -Check (eq_refl false <: - infinity < - infinity = false). -Check (eq_refl true <: - infinity <= - infinity = true). -Check (eq_refl true <: - infinity <= - infinity = true). +Check (eq_refl true <: - infinity =? - infinity = true). +Check (eq_refl true <: - infinity =? - infinity = true). +Check (eq_refl false <: - infinity <? - infinity = false). +Check (eq_refl false <: - infinity <? - infinity = false). +Check (eq_refl true <: - infinity <=? - infinity = true). +Check (eq_refl true <: - infinity <=? - infinity = true). Check (eq_refl FEq <: - infinity ?= - infinity = FEq). Check (eq_refl FEq <: - infinity ?= - infinity = FEq). -Check (eq_refl true <<: - infinity == - infinity = true). -Check (eq_refl true <<: - infinity == - infinity = true). -Check (eq_refl false <<: - infinity < - infinity = false). -Check (eq_refl false <<: - infinity < - infinity = false). -Check (eq_refl true <<: - infinity <= - infinity = true). -Check (eq_refl true <<: - infinity <= - infinity = true). +Check (eq_refl true <<: - infinity =? - infinity = true). +Check (eq_refl true <<: - infinity =? - infinity = true). +Check (eq_refl false <<: - infinity <? - infinity = false). +Check (eq_refl false <<: - infinity <? - infinity = false). +Check (eq_refl true <<: - infinity <=? - infinity = true). +Check (eq_refl true <<: - infinity <=? - infinity = true). Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). -Check (eq_refl false : min_denorm == min_norm = false). -Check (eq_refl false : min_norm == min_denorm = false). -Check (eq_refl true : min_denorm < min_norm = true). -Check (eq_refl false : min_norm < min_denorm = false). -Check (eq_refl true : min_denorm <= min_norm = true). -Check (eq_refl false : min_norm <= min_denorm = false). +Check (eq_refl false : min_denorm =? min_norm = false). +Check (eq_refl false : min_norm =? min_denorm = false). +Check (eq_refl true : min_denorm <? min_norm = true). +Check (eq_refl false : min_norm <? min_denorm = false). +Check (eq_refl true : min_denorm <=? min_norm = true). +Check (eq_refl false : min_norm <=? min_denorm = false). Check (eq_refl FLt : min_denorm ?= min_norm = FLt). Check (eq_refl FGt : min_norm ?= min_denorm = FGt). -Check (eq_refl false <: min_denorm == min_norm = false). -Check (eq_refl false <: min_norm == min_denorm = false). -Check (eq_refl true <: min_denorm < min_norm = true). -Check (eq_refl false <: min_norm < min_denorm = false). -Check (eq_refl true <: min_denorm <= min_norm = true). -Check (eq_refl false <: min_norm <= min_denorm = false). +Check (eq_refl false <: min_denorm =? min_norm = false). +Check (eq_refl false <: min_norm =? min_denorm = false). +Check (eq_refl true <: min_denorm <? min_norm = true). +Check (eq_refl false <: min_norm <? min_denorm = false). +Check (eq_refl true <: min_denorm <=? min_norm = true). +Check (eq_refl false <: min_norm <=? min_denorm = false). Check (eq_refl FLt <: min_denorm ?= min_norm = FLt). Check (eq_refl FGt <: min_norm ?= min_denorm = FGt). -Check (eq_refl false <<: min_denorm == min_norm = false). -Check (eq_refl false <<: min_norm == min_denorm = false). -Check (eq_refl true <<: min_denorm < min_norm = true). -Check (eq_refl false <<: min_norm < min_denorm = false). -Check (eq_refl true <<: min_denorm <= min_norm = true). -Check (eq_refl false <<: min_norm <= min_denorm = false). +Check (eq_refl false <<: min_denorm =? min_norm = false). +Check (eq_refl false <<: min_norm =? min_denorm = false). +Check (eq_refl true <<: min_denorm <? min_norm = true). +Check (eq_refl false <<: min_norm <? min_denorm = false). +Check (eq_refl true <<: min_denorm <=? min_norm = true). +Check (eq_refl false <<: min_norm <=? min_denorm = false). Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt). Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt). -Check (eq_refl false : min_denorm == one = false). -Check (eq_refl false : one == min_denorm = false). -Check (eq_refl true : min_denorm < one = true). -Check (eq_refl false : one < min_denorm = false). -Check (eq_refl true : min_denorm <= one = true). -Check (eq_refl false : one <= min_denorm = false). +Check (eq_refl false : min_denorm =? one = false). +Check (eq_refl false : one =? min_denorm = false). +Check (eq_refl true : min_denorm <? one = true). +Check (eq_refl false : one <? min_denorm = false). +Check (eq_refl true : min_denorm <=? one = true). +Check (eq_refl false : one <=? min_denorm = false). Check (eq_refl FLt : min_denorm ?= one = FLt). Check (eq_refl FGt : one ?= min_denorm = FGt). -Check (eq_refl false <: min_denorm == one = false). -Check (eq_refl false <: one == min_denorm = false). -Check (eq_refl true <: min_denorm < one = true). -Check (eq_refl false <: one < min_denorm = false). -Check (eq_refl true <: min_denorm <= one = true). -Check (eq_refl false <: one <= min_denorm = false). +Check (eq_refl false <: min_denorm =? one = false). +Check (eq_refl false <: one =? min_denorm = false). +Check (eq_refl true <: min_denorm <? one = true). +Check (eq_refl false <: one <? min_denorm = false). +Check (eq_refl true <: min_denorm <=? one = true). +Check (eq_refl false <: one <=? min_denorm = false). Check (eq_refl FLt <: min_denorm ?= one = FLt). Check (eq_refl FGt <: one ?= min_denorm = FGt). -Check (eq_refl false <<: min_denorm == one = false). -Check (eq_refl false <<: one == min_denorm = false). -Check (eq_refl true <<: min_denorm < one = true). -Check (eq_refl false <<: one < min_denorm = false). -Check (eq_refl true <<: min_denorm <= one = true). -Check (eq_refl false <<: one <= min_denorm = false). +Check (eq_refl false <<: min_denorm =? one = false). +Check (eq_refl false <<: one =? min_denorm = false). +Check (eq_refl true <<: min_denorm <? one = true). +Check (eq_refl false <<: one <? min_denorm = false). +Check (eq_refl true <<: min_denorm <=? one = true). +Check (eq_refl false <<: one <=? min_denorm = false). Check (eq_refl FLt <<: min_denorm ?= one = FLt). Check (eq_refl FGt <<: one ?= min_denorm = FGt). -Check (eq_refl false : min_norm == one = false). -Check (eq_refl false : one == min_norm = false). -Check (eq_refl true : min_norm < one = true). -Check (eq_refl false : one < min_norm = false). -Check (eq_refl true : min_norm <= one = true). -Check (eq_refl false : one <= min_norm = false). +Check (eq_refl false : min_norm =? one = false). +Check (eq_refl false : one =? min_norm = false). +Check (eq_refl true : min_norm <? one = true). +Check (eq_refl false : one <? min_norm = false). +Check (eq_refl true : min_norm <=? one = true). +Check (eq_refl false : one <=? min_norm = false). Check (eq_refl FLt : min_norm ?= one = FLt). Check (eq_refl FGt : one ?= min_norm = FGt). -Check (eq_refl false <: min_norm == one = false). -Check (eq_refl false <: one == min_norm = false). -Check (eq_refl true <: min_norm < one = true). -Check (eq_refl false <: one < min_norm = false). -Check (eq_refl true <: min_norm <= one = true). -Check (eq_refl false <: one <= min_norm = false). +Check (eq_refl false <: min_norm =? one = false). +Check (eq_refl false <: one =? min_norm = false). +Check (eq_refl true <: min_norm <? one = true). +Check (eq_refl false <: one <? min_norm = false). +Check (eq_refl true <: min_norm <=? one = true). +Check (eq_refl false <: one <=? min_norm = false). Check (eq_refl FLt <: min_norm ?= one = FLt). Check (eq_refl FGt <: one ?= min_norm = FGt). -Check (eq_refl false <<: min_norm == one = false). -Check (eq_refl false <<: one == min_norm = false). -Check (eq_refl true <<: min_norm < one = true). -Check (eq_refl false <<: one < min_norm = false). -Check (eq_refl true <<: min_norm <= one = true). -Check (eq_refl false <<: one <= min_norm = false). +Check (eq_refl false <<: min_norm =? one = false). +Check (eq_refl false <<: one =? min_norm = false). +Check (eq_refl true <<: min_norm <? one = true). +Check (eq_refl false <<: one <? min_norm = false). +Check (eq_refl true <<: min_norm <=? one = true). +Check (eq_refl false <<: one <=? min_norm = false). Check (eq_refl FLt <<: min_norm ?= one = FLt). Check (eq_refl FGt <<: one ?= min_norm = FGt). -Check (eq_refl false : one == infinity = false). -Check (eq_refl false : infinity == one = false). -Check (eq_refl true : one < infinity = true). -Check (eq_refl false : infinity < one = false). -Check (eq_refl true : one <= infinity = true). -Check (eq_refl false : infinity <= one = false). +Check (eq_refl false : one =? infinity = false). +Check (eq_refl false : infinity =? one = false). +Check (eq_refl true : one <? infinity = true). +Check (eq_refl false : infinity <? one = false). +Check (eq_refl true : one <=? infinity = true). +Check (eq_refl false : infinity <=? one = false). Check (eq_refl FLt : one ?= infinity = FLt). Check (eq_refl FGt : infinity ?= one = FGt). -Check (eq_refl false <: one == infinity = false). -Check (eq_refl false <: infinity == one = false). -Check (eq_refl true <: one < infinity = true). -Check (eq_refl false <: infinity < one = false). -Check (eq_refl true <: one <= infinity = true). -Check (eq_refl false <: infinity <= one = false). +Check (eq_refl false <: one =? infinity = false). +Check (eq_refl false <: infinity =? one = false). +Check (eq_refl true <: one <? infinity = true). +Check (eq_refl false <: infinity <? one = false). +Check (eq_refl true <: one <=? infinity = true). +Check (eq_refl false <: infinity <=? one = false). Check (eq_refl FLt <: one ?= infinity = FLt). Check (eq_refl FGt <: infinity ?= one = FGt). -Check (eq_refl false <<: one == infinity = false). -Check (eq_refl false <<: infinity == one = false). -Check (eq_refl true <<: one < infinity = true). -Check (eq_refl false <<: infinity < one = false). -Check (eq_refl true <<: one <= infinity = true). -Check (eq_refl false <<: infinity <= one = false). +Check (eq_refl false <<: one =? infinity = false). +Check (eq_refl false <<: infinity =? one = false). +Check (eq_refl true <<: one <? infinity = true). +Check (eq_refl false <<: infinity <? one = false). +Check (eq_refl true <<: one <=? infinity = true). +Check (eq_refl false <<: infinity <=? one = false). Check (eq_refl FLt <<: one ?= infinity = FLt). Check (eq_refl FGt <<: infinity ?= one = FGt). -Check (eq_refl false : - infinity == infinity = false). -Check (eq_refl false : infinity == - infinity = false). -Check (eq_refl true : - infinity < infinity = true). -Check (eq_refl false : infinity < - infinity = false). -Check (eq_refl true : - infinity <= infinity = true). -Check (eq_refl false : infinity <= - infinity = false). +Check (eq_refl false : - infinity =? infinity = false). +Check (eq_refl false : infinity =? - infinity = false). +Check (eq_refl true : - infinity <? infinity = true). +Check (eq_refl false : infinity <? - infinity = false). +Check (eq_refl true : - infinity <=? infinity = true). +Check (eq_refl false : infinity <=? - infinity = false). Check (eq_refl FLt : - infinity ?= infinity = FLt). Check (eq_refl FGt : infinity ?= - infinity = FGt). -Check (eq_refl false <: - infinity == infinity = false). -Check (eq_refl false <: infinity == - infinity = false). -Check (eq_refl true <: - infinity < infinity = true). -Check (eq_refl false <: infinity < - infinity = false). -Check (eq_refl true <: - infinity <= infinity = true). -Check (eq_refl false <: infinity <= - infinity = false). +Check (eq_refl false <: - infinity =? infinity = false). +Check (eq_refl false <: infinity =? - infinity = false). +Check (eq_refl true <: - infinity <? infinity = true). +Check (eq_refl false <: infinity <? - infinity = false). +Check (eq_refl true <: - infinity <=? infinity = true). +Check (eq_refl false <: infinity <=? - infinity = false). Check (eq_refl FLt <: - infinity ?= infinity = FLt). Check (eq_refl FGt <: infinity ?= - infinity = FGt). -Check (eq_refl false <<: - infinity == infinity = false). -Check (eq_refl false <<: infinity == - infinity = false). -Check (eq_refl true <<: - infinity < infinity = true). -Check (eq_refl false <<: infinity < - infinity = false). -Check (eq_refl true <<: - infinity <= infinity = true). -Check (eq_refl false <<: infinity <= - infinity = false). +Check (eq_refl false <<: - infinity =? infinity = false). +Check (eq_refl false <<: infinity =? - infinity = false). +Check (eq_refl true <<: - infinity <? infinity = true). +Check (eq_refl false <<: infinity <? - infinity = false). +Check (eq_refl true <<: - infinity <=? infinity = true). +Check (eq_refl false <<: infinity <=? - infinity = false). Check (eq_refl FLt <<: - infinity ?= infinity = FLt). Check (eq_refl FGt <<: infinity ?= - infinity = FGt). -Check (eq_refl false : - infinity == one = false). -Check (eq_refl false : one == - infinity = false). -Check (eq_refl true : - infinity < one = true). -Check (eq_refl false : one < - infinity = false). -Check (eq_refl true : - infinity <= one = true). -Check (eq_refl false : one <= - infinity = false). +Check (eq_refl false : - infinity =? one = false). +Check (eq_refl false : one =? - infinity = false). +Check (eq_refl true : - infinity <? one = true). +Check (eq_refl false : one <? - infinity = false). +Check (eq_refl true : - infinity <=? one = true). +Check (eq_refl false : one <=? - infinity = false). Check (eq_refl FLt : - infinity ?= one = FLt). Check (eq_refl FGt : one ?= - infinity = FGt). -Check (eq_refl false <: - infinity == one = false). -Check (eq_refl false <: one == - infinity = false). -Check (eq_refl true <: - infinity < one = true). -Check (eq_refl false <: one < - infinity = false). -Check (eq_refl true <: - infinity <= one = true). -Check (eq_refl false <: one <= - infinity = false). +Check (eq_refl false <: - infinity =? one = false). +Check (eq_refl false <: one =? - infinity = false). +Check (eq_refl true <: - infinity <? one = true). +Check (eq_refl false <: one <? - infinity = false). +Check (eq_refl true <: - infinity <=? one = true). +Check (eq_refl false <: one <=? - infinity = false). Check (eq_refl FLt <: - infinity ?= one = FLt). Check (eq_refl FGt <: one ?= - infinity = FGt). -Check (eq_refl false <<: - infinity == one = false). -Check (eq_refl false <<: one == - infinity = false). -Check (eq_refl true <<: - infinity < one = true). -Check (eq_refl false <<: one < - infinity = false). -Check (eq_refl true <<: - infinity <= one = true). -Check (eq_refl false <<: one <= - infinity = false). +Check (eq_refl false <<: - infinity =? one = false). +Check (eq_refl false <<: one =? - infinity = false). +Check (eq_refl true <<: - infinity <? one = true). +Check (eq_refl false <<: one <? - infinity = false). +Check (eq_refl true <<: - infinity <=? one = true). +Check (eq_refl false <<: one <=? - infinity = false). Check (eq_refl FLt <<: - infinity ?= one = FLt). Check (eq_refl FGt <<: one ?= - infinity = FGt). diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh index cd87eb4e5b..6e3dd6d04b 100755 --- a/test-suite/primitive/float/gen_compare.sh +++ b/test-suite/primitive/float/gen_compare.sh @@ -20,7 +20,7 @@ genTest() { echo >&2 "genTest expects 10 arguments" fi TACTICS=(":" "<:" "<<:") - OPS=("==" "<" "<=" "?=") + OPS=("=?" "<?" "<=?" "?=") x="$1" y="$2" OPS1=("$3" "$4" "$5" "$6") # for x y diff --git a/test-suite/primitive/uint63/eqb.v b/test-suite/primitive/uint63/eqb.v index dcc0b71f6d..43c98e2b6f 100644 --- a/test-suite/primitive/uint63/eqb.v +++ b/test-suite/primitive/uint63/eqb.v @@ -4,14 +4,14 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 1 == 1 = true). -Check (eq_refl true <: 1 == 1 = true). -Check (eq_refl true <<: 1 == 1 = true). -Definition compute1 := Eval compute in 1 == 1. +Check (eq_refl : 1 =? 1 = true). +Check (eq_refl true <: 1 =? 1 = true). +Check (eq_refl true <<: 1 =? 1 = true). +Definition compute1 := Eval compute in 1 =? 1. Check (eq_refl compute1 : true = true). -Check (eq_refl : 9223372036854775807 == 0 = false). -Check (eq_refl false <: 9223372036854775807 == 0 = false). -Check (eq_refl false <<: 9223372036854775807 == 0 = false). -Definition compute2 := Eval compute in 9223372036854775807 == 0. +Check (eq_refl : 9223372036854775807 =? 0 = false). +Check (eq_refl false <: 9223372036854775807 =? 0 = false). +Check (eq_refl false <<: 9223372036854775807 =? 0 = false). +Definition compute2 := Eval compute in 9223372036854775807 =? 0. Check (eq_refl compute2 : false = false). diff --git a/test-suite/primitive/uint63/leb.v b/test-suite/primitive/uint63/leb.v index 5354919978..e5142282ae 100644 --- a/test-suite/primitive/uint63/leb.v +++ b/test-suite/primitive/uint63/leb.v @@ -4,20 +4,20 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 1 <= 1 = true). -Check (eq_refl true <: 1 <= 1 = true). -Check (eq_refl true <<: 1 <= 1 = true). -Definition compute1 := Eval compute in 1 <= 1. +Check (eq_refl : 1 <=? 1 = true). +Check (eq_refl true <: 1 <=? 1 = true). +Check (eq_refl true <<: 1 <=? 1 = true). +Definition compute1 := Eval compute in 1 <=? 1. Check (eq_refl compute1 : true = true). -Check (eq_refl : 1 <= 2 = true). -Check (eq_refl true <: 1 <= 2 = true). -Check (eq_refl true <<: 1 <= 2 = true). -Definition compute2 := Eval compute in 1 <= 2. +Check (eq_refl : 1 <=? 2 = true). +Check (eq_refl true <: 1 <=? 2 = true). +Check (eq_refl true <<: 1 <=? 2 = true). +Definition compute2 := Eval compute in 1 <=? 2. Check (eq_refl compute2 : true = true). -Check (eq_refl : 9223372036854775807 <= 0 = false). -Check (eq_refl false <: 9223372036854775807 <= 0 = false). -Check (eq_refl false <<: 9223372036854775807 <= 0 = false). -Definition compute3 := Eval compute in 9223372036854775807 <= 0. +Check (eq_refl : 9223372036854775807 <=? 0 = false). +Check (eq_refl false <: 9223372036854775807 <=? 0 = false). +Check (eq_refl false <<: 9223372036854775807 <=? 0 = false). +Definition compute3 := Eval compute in 9223372036854775807 <=? 0. Check (eq_refl compute3 : false = false). diff --git a/test-suite/primitive/uint63/ltb.v b/test-suite/primitive/uint63/ltb.v index 7ae5ac6493..50cef6be66 100644 --- a/test-suite/primitive/uint63/ltb.v +++ b/test-suite/primitive/uint63/ltb.v @@ -4,20 +4,20 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 1 < 1 = false). -Check (eq_refl false <: 1 < 1 = false). -Check (eq_refl false <<: 1 < 1 = false). -Definition compute1 := Eval compute in 1 < 1. +Check (eq_refl : 1 <? 1 = false). +Check (eq_refl false <: 1 <? 1 = false). +Check (eq_refl false <<: 1 <? 1 = false). +Definition compute1 := Eval compute in 1 <? 1. Check (eq_refl compute1 : false = false). -Check (eq_refl : 1 < 2 = true). -Check (eq_refl true <: 1 < 2 = true). -Check (eq_refl true <<: 1 < 2 = true). -Definition compute2 := Eval compute in 1 < 2. +Check (eq_refl : 1 <? 2 = true). +Check (eq_refl true <: 1 <? 2 = true). +Check (eq_refl true <<: 1 <? 2 = true). +Definition compute2 := Eval compute in 1 <? 2. Check (eq_refl compute2 : true = true). -Check (eq_refl : 9223372036854775807 < 0 = false). -Check (eq_refl false <: 9223372036854775807 < 0 = false). -Check (eq_refl false <<: 9223372036854775807 < 0 = false). -Definition compute3 := Eval compute in 9223372036854775807 < 0. +Check (eq_refl : 9223372036854775807 <? 0 = false). +Check (eq_refl false <: 9223372036854775807 <? 0 = false). +Check (eq_refl false <<: 9223372036854775807 <? 0 = false). +Definition compute3 := Eval compute in 9223372036854775807 <? 0. Check (eq_refl compute3 : false = false). diff --git a/test-suite/primitive/uint63/mod.v b/test-suite/primitive/uint63/mod.v index 5307eed493..3ad6312c2c 100644 --- a/test-suite/primitive/uint63/mod.v +++ b/test-suite/primitive/uint63/mod.v @@ -4,14 +4,14 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 6 \% 3 = 0). -Check (eq_refl 0 <: 6 \% 3 = 0). -Check (eq_refl 0 <<: 6 \% 3 = 0). -Definition compute1 := Eval compute in 6 \% 3. +Check (eq_refl : 6 mod 3 = 0). +Check (eq_refl 0 <: 6 mod 3 = 0). +Check (eq_refl 0 <<: 6 mod 3 = 0). +Definition compute1 := Eval compute in 6 mod 3. Check (eq_refl compute1 : 0 = 0). -Check (eq_refl : 5 \% 3 = 2). -Check (eq_refl 2 <: 5 \% 3 = 2). -Check (eq_refl 2 <<: 5 \% 3 = 2). -Definition compute2 := Eval compute in 5 \% 3. +Check (eq_refl : 5 mod 3 = 2). +Check (eq_refl 2 <: 5 mod 3 = 2). +Check (eq_refl 2 <<: 5 mod 3 = 2). +Definition compute2 := Eval compute in 5 mod 3. Check (eq_refl compute2 : 2 = 2). diff --git a/test-suite/primitive/uint63/unsigned.v b/test-suite/primitive/uint63/unsigned.v index 82920bd201..6224e9d15b 100644 --- a/test-suite/primitive/uint63/unsigned.v +++ b/test-suite/primitive/uint63/unsigned.v @@ -11,8 +11,8 @@ Check (eq_refl 0 <<: 1/(0-1) = 0). Definition compute1 := Eval compute in 1/(0-1). Check (eq_refl compute1 : 0 = 0). -Check (eq_refl : 3 \% (0-1) = 3). -Check (eq_refl 3 <: 3 \% (0-1) = 3). -Check (eq_refl 3 <<: 3 \% (0-1) = 3). -Definition compute2 := Eval compute in 3 \% (0-1). +Check (eq_refl : 3 mod (0-1) = 3). +Check (eq_refl 3 <: 3 mod (0-1) = 3). +Check (eq_refl 3 <<: 3 mod (0-1) = 3). +Definition compute2 := Eval compute in 3 mod (0-1). Check (eq_refl compute2 : 3 = 3). diff --git a/test-suite/ssr/noting_to_inject.v b/test-suite/ssr/noting_to_inject.v new file mode 100644 index 0000000000..95bbd3e777 --- /dev/null +++ b/test-suite/ssr/noting_to_inject.v @@ -0,0 +1,9 @@ +Require Import ssreflect ssrfun ssrbool. + + +Goal forall b : bool, b -> False. +Set Warnings "+spurious-ssr-injection". +Fail move=> b []. +Set Warnings "-spurious-ssr-injection". +move=> b []. +Abort. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 563651cfa5..7acaa92b89 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -190,7 +190,7 @@ Record Monad {m : Type -> Type} := { Print Visibility. Print unit. -Arguments unit {m m0 α}. +Arguments unit {m _ α}. Arguments Monad : clear implicits. Notation "'return' t" := (unit t). |