diff options
Diffstat (limited to 'test-suite')
23 files changed, 472 insertions, 298 deletions
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_12566_1.v b/test-suite/bugs/closed/bug_12566_1.v new file mode 100644 index 0000000000..22d95949bb --- /dev/null +++ b/test-suite/bugs/closed/bug_12566_1.v @@ -0,0 +1,16 @@ + +Class C (n:nat) := c{}. + +Instance c0 : C 0 := {}. + +Definition x := 0. + +Opaque x. + +Type _ : C x. +(* this is maybe wrong behaviour, if it changes just update the test *) + +Hint Opaque x : typeclass_instances. +Transparent x. + +Fail Type _ : C x. 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/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_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/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. |