diff options
Diffstat (limited to 'test-suite/output')
38 files changed, 628 insertions, 212 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 7c9b1e27..629a1ab6 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,94 +1,110 @@ -minus : nat -> nat -> nat +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus avoiding to expose match constructs -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +The reduction tactics unfold Nat.sub but avoid exposing match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus when applied to 1 argument - avoiding to expose match constructs -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +The reduction tactics unfold Nat.sub when applied to 1 argument + but avoid exposing match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus +The reduction tactics unfold Nat.sub when the 1st argument evaluates to a constructor and - when applied to 1 argument avoiding to expose match constructs -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat + when applied to 1 argument but avoid exposing match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus - when the 1st and 2nd arguments evaluate to a constructor and - when applied to 2 arguments -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +The reduction tactics unfold Nat.sub when the 1st and + 2nd arguments evaluate to a constructor and when applied to 2 arguments +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus - when the 1st and 2nd arguments evaluate to a constructor -minus is transparent -Expands to: Constant Coq.Init.Peano.minus +The reduction tactics unfold Nat.sub when the 1st and + 2nd arguments evaluate to a constructor +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub pf : forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 +pf is not universe polymorphic Arguments D2, C2 are implicit Arguments D1, C1 are implicit and maximally inserted Argument scopes are [foo_scope type_scope _ _ _ _ _] -The simpl tactic never unfolds pf +The reduction tactics never unfold pf pf is transparent Expands to: Constant Top.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C +fcomp is not universe polymorphic Arguments A, B, C are implicit and maximally inserted Argument scopes are [type_scope type_scope type_scope _ _ _] -The simpl tactic unfolds fcomp when applied to 6 arguments +The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Top.fcomp volatile : nat -> nat +volatile is not universe polymorphic Argument scope is [nat_scope] -The simpl tactic always unfolds volatile +The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Top.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] f is transparent Expands to: Constant Top.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 3rd, 4th and 5th arguments evaluate to a constructor +The reduction tactics unfold f when the 3rd, 4th and + 5th arguments evaluate to a constructor f is transparent Expands to: Constant Top.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 4th, 5th and 6th arguments evaluate to a constructor +The reduction tactics unfold f when the 4th, 5th and + 6th arguments evaluate to a constructor f is transparent Expands to: Constant Top.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 5th, 6th and 7th arguments evaluate to a constructor +The reduction tactics unfold f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Top.f + = forall v : unit, f 0 0 5 v 3 = 2 + : Prop + = 2 = 2 + : Prop f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -The simpl tactic unfolds f - when the 5th, 6th and 7th arguments evaluate to a constructor +f is not universe polymorphic +The reduction tactics unfold f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Top.f forall w : r, w 3 true = tt diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 573cfdab..05eeaac6 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -1,13 +1,13 @@ -Arguments minus n m : simpl nomatch. -About minus. -Arguments minus n / m : simpl nomatch. -About minus. -Arguments minus !n / m : simpl nomatch. -About minus. -Arguments minus !n !m /. -About minus. -Arguments minus !n !m. -About minus. +Arguments Nat.sub n m : simpl nomatch. +About Nat.sub. +Arguments Nat.sub n / m : simpl nomatch. +About Nat.sub. +Arguments Nat.sub !n / m : simpl nomatch. +About Nat.sub. +Arguments Nat.sub !n !m /. +About Nat.sub. +Arguments Nat.sub !n !m. +About Nat.sub. Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := fun x => (f (fst x), g (snd x)). Delimit Scope foo_scope with F. @@ -36,13 +36,15 @@ End S2. About f. End S1. About f. +Eval cbn in forall v, f 0 0 5 v 3 = 2. +Eval cbn in f 0 0 5 tt 3 = 2. Arguments f : clear implicits and scopes. About f. Record r := { pi :> nat -> bool -> unit }. Notation "$" := 3 (only parsing) : foo_scope. Notation "$" := true (only parsing) : bar_scope. Delimit Scope bar_scope with B. -Arguments pi _ _%F _%B. +Arguments pi _ _%F _%B. Check (forall w : r, pi w $ $ = tt). Fail Check (forall w : r, w $ $ = tt). Axiom w : r. diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 756e8ede..71d5fc78 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,61 +1,70 @@ a : bool -> bool +a is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable a b : bool -> bool +b is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable b negb'' : bool -> bool +negb'' is not universe polymorphic Argument scope is [bool_scope] negb'' is transparent Expands to: Constant Top.A.B.negb'' negb' : bool -> bool +negb' is not universe polymorphic Argument scope is [bool_scope] negb' is transparent Expands to: Constant Top.A.negb' negb : bool -> bool +negb is not universe polymorphic Argument scope is [bool_scope] negb is transparent Expands to: Constant Coq.Init.Datatypes.negb -Warning: Arguments Scope is deprecated; use Arguments instead -Warning: Arguments Scope is deprecated; use Arguments instead -Warning: Arguments Scope is deprecated; use Arguments instead -Warning: Arguments Scope is deprecated; use Arguments instead -Warning: Arguments Scope is deprecated; use Arguments instead a : bool -> bool +a is not universe polymorphic Expands to: Variable a b : bool -> bool +b is not universe polymorphic Expands to: Variable b negb : bool -> bool +negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool +negb' is not universe polymorphic negb' is transparent Expands to: Constant Top.A.negb' negb'' : bool -> bool +negb'' is not universe polymorphic negb'' is transparent Expands to: Constant Top.A.B.negb'' a : bool -> bool +a is not universe polymorphic Expands to: Variable a negb : bool -> bool +negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool +negb' is not universe polymorphic negb' is transparent Expands to: Constant Top.negb' negb'' : bool -> bool +negb'' is not universe polymorphic negb'' is transparent Expands to: Constant Top.negb'' diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 17c80d13..c29f5649 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -6,7 +6,7 @@ The command has indeed failed with message: Argument A renamed to T. @eq_refl : forall (B : Type) (y : B), y = y -eq_refl +@eq_refl nat : forall x : nat, x = x Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x @@ -20,6 +20,7 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x +eq_refl is not universe polymorphic Arguments are renamed to B, y When applied to no arguments: Arguments B, y are implicit and maximally inserted @@ -35,6 +36,7 @@ For myEq: Argument scopes are [type_scope _ _] For myrefl: Argument scopes are [type_scope _ _] myrefl : forall (B : Type) (x : A), B -> myEq B x x +myrefl is not universe polymorphic Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] @@ -47,19 +49,21 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] -The simpl tactic unfolds myplus - when the 2nd and 3rd arguments evaluate to a constructor +The reduction tactics unfold myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.Test1.myplus -myplus +@myplus : forall Z : Type, Z -> nat -> nat -> nat Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x @@ -70,6 +74,7 @@ For myEq: Argument scopes are [type_scope type_scope _ _] For myrefl: Argument scopes are [type_scope type_scope _ _] myrefl : forall (A B : Type) (x : A), B -> myEq A B x x +myrefl is not universe polymorphic Arguments are renamed to A, C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope type_scope _ _] @@ -84,19 +89,21 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] -The simpl tactic unfolds myplus - when the 2nd and 3rd arguments evaluate to a constructor +The reduction tactics unfold myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.myplus -myplus +@myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: => Error: All arguments lists must declare the same names. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 1ec02c56..d5903483 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -2,13 +2,23 @@ t_rect = fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => fix F (t : t) : P t := match t as t0 return (P t0) with - | k _ x0 => f x0 (F x0) + | @k _ x0 => f x0 (F x0) end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t + +t_rect is not universe polymorphic + = fun d : TT => match d with + | @CTT _ _ b => b + end + : TT -> 0 = 0 + = fun d : TT => match d with + | @CTT _ _ b => b + end + : TT -> 0 = 0 proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => -match eq_nat_dec x y with +match Nat.eq_dec x y with | left eqprf => match eqprf in (_ = z) return (P z) with | eq_refl => def end @@ -16,6 +26,7 @@ match eq_nat_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y +proj is not universe polymorphic Argument scopes are [nat_scope nat_scope _ _ _] foo = fix foo (A : Type) (l : list A) {struct l} : option A := @@ -26,6 +37,29 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A +foo is not universe polymorphic Argument scopes are [type_scope list_scope] +uncast = +fun (A : Type) (x : I A) => match x with + | x0 <: _ => x0 + end + : forall A : Type, I A -> A + +uncast is not universe polymorphic +Argument scopes are [type_scope _] foo' = if A 0 then true else false : bool + +foo' is not universe polymorphic +f = +fun H : B => +match H with +| AC x => + (let b0 := b in + if b0 as b return (P b -> True) + then fun _ : P true => Logic.I + else fun _ : P false => Logic.I) x +end + : B -> True + +f is not universe polymorphic diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index b6337586..4116a5eb 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -5,6 +5,11 @@ Inductive t : Set := Print t_rect. +Record TT : Type := CTT { f1 := 0 : nat; f2: nat; f3 : f1=f1 }. + +Eval cbv in fun d:TT => match d return 0 = 0 with CTT a _ b => b end. +Eval lazy in fun d:TT => match d return 0 = 0 with CTT a _ b => b end. + (* Do not contract nested patterns with dependent return type *) (* see bug #1699 *) @@ -34,6 +39,18 @@ Fixpoint foo (A:Type) (l:list A) : option A := Print foo. +(* Accept and use notation with binded parameters *) + +Inductive I (A: Type) : Type := C : A -> I A. +Notation "x <: T" := (C T x) (at level 38). + +Definition uncast A (x : I A) := +match x with + | x <: _ => x +end. + +Print uncast. + (* Do not duplicate the matched term *) Axiom A : nat -> bool. @@ -46,3 +63,17 @@ Definition foo' := Print foo'. +(* Was bug #3293 (eta-expansion at "match" printing time was failing because + of let-in's interpreted as being part of the expansion) *) + +Variable b : bool. +Variable P : bool -> Prop. +Inductive B : Prop := AC : P b -> B. +Definition f : B -> True. + +Proof. +intros []. +destruct b as [|] ; intros _ ; exact Logic.I. +Defined. + +Print f. diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index f61b7ecf..bcc37b63 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -1,2 +1,7 @@ The command has indeed failed with message: => Error: The field t is missing in Top.M. +The command has indeed failed with message: +=> Error: Unable to unify "nat" with "True". +The command has indeed failed with message: +=> In nested Ltac calls to "f" and "apply x", last call failed. +Error: Unable to unify "nat" with "True". diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index 75763f3b..352c8738 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -7,3 +7,12 @@ Parameter t:Type. End S. Module M : S. Fail End M. + +(* A simple check of how Ltac trace are used or not *) +(* Unfortunately, cannot test error location... *) + +Ltac f x := apply x. +Goal True. +Fail simpl; apply 0. +Fail simpl; f 0. +Abort. diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out index 2f756cbb..483a9ea7 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1,3 +1,5 @@ -Existential 1 = ?10 : [q : nat n : nat m : nat |- n = ?9] -Existential 2 = ?9 : [n : nat m : nat |- nat] -Existential 3 = ?7 : [p : nat q := S p : nat n : nat m : nat |- ?9 = m] +Existential 1 = +?Goal0 : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +Existential 2 = +?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) +Existential 3 = ?e : [q : nat n : nat m : nat |- n = ?y] diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index f5610efc..6c514b16 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -22,8 +22,8 @@ Inductive hole (A:Set) : Set := Hole | Hole2. Definition wrong_id (A B : Set) (x:hole A) : hole B := match x with - | Hole => @Hole _ - | Hole2 => @Hole2 _ + | Hole _ => @Hole _ + | Hole2 _ => @Hole2 _ end. Extraction wrong_id. (** should _not_ be optimized as an identity *) @@ -114,9 +114,9 @@ Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode) | Some oc => match f w with | DecInst i => DecInst (g i oc) - | DecError m => @DecError inst m - | DecUndefined => @DecUndefined inst - | DecUnpredictable => @DecUnpredictable inst + | DecError _ m => @DecError inst m + | DecUndefined _ => @DecUndefined inst + | DecUnpredictable _ => @DecUnpredictable inst end | None => @DecUndefined inst end. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 3b65003c..0b0f501f 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,6 +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 +d2 is not universe polymorphic Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] map id (1 :: nil) diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 55017469..bbfd3405 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,5 +1,5 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := - exist2 : forall x : A, P x -> Q x -> {x | P x & Q x} + exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} For sig2: Argument A is implicit For exist2: Argument A is implicit diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out index 5831c9f4..e99d9fde 100644 --- a/test-suite/output/Intuition.out +++ b/test-suite/output/Intuition.out @@ -1,7 +1,6 @@ 1 subgoal - m : Z - n : Z + m, n : Z H : (m >= n)%Z ============================ (m >= m)%Z diff --git a/test-suite/output/Match_subterm.out b/test-suite/output/Match_subterm.out index 951a98db..c99c8905 100644 --- a/test-suite/output/Match_subterm.out +++ b/test-suite/output/Match_subterm.out @@ -1,5 +1,7 @@ (0 = 1) +(eq 0) eq +@eq nat 0 1 diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out index b1883ec0..c11621d7 100644 --- a/test-suite/output/Nametab.out +++ b/test-suite/output/Nametab.out @@ -7,15 +7,15 @@ Constant Top.Q.N.K.foo Constant Top.Q.N.K.foo Constant Top.Q.N.K.foo (shorter name to refer to it in current context is Q.N.K.foo) -No module is referred to by basename K -No module is referred to by name N.K +Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K) +Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K) Module Top.Q.N.K -Module Top.Q.N.K -No module is referred to by basename N -Module Top.Q.N +Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K) +Module Top.Q.N (shorter name to refer to it in current context is Q.N) Module Top.Q.N +Module Top.Q.N (shorter name to refer to it in current context is Q.N) Module Top.Q -Module Top.Q +Module Top.Q (shorter name to refer to it in current context is Q) Constant Top.Q.N.K.foo (shorter name to refer to it in current context is K.foo) Constant Top.Q.N.K.foo @@ -26,11 +26,11 @@ Constant Top.Q.N.K.foo Constant Top.Q.N.K.foo (shorter name to refer to it in current context is K.foo) Module Top.Q.N.K -No module is referred to by name N.K -Module Top.Q.N.K -Module Top.Q.N.K -No module is referred to by basename N -Module Top.Q.N +Module Top.Q.N.K (shorter name to refer to it in current context is K) +Module Top.Q.N.K (shorter name to refer to it in current context is K) +Module Top.Q.N.K (shorter name to refer to it in current context is K) +Module Top.Q.N (shorter name to refer to it in current context is Q.N) Module Top.Q.N +Module Top.Q.N (shorter name to refer to it in current context is Q.N) Module Top.Q -Module Top.Q +Module Top.Q (shorter name to refer to it in current context is Q) diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index df510063..f0d2562e 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -6,12 +6,8 @@ (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat - H : forall x5 x6 : nat, x5 + x1 = x4 + x6 + x3, x, x1, x4, x0 : nat + H : forall x x3 : nat, x + x1 = x4 + x3 ============================ x + x1 = x4 + x0 1 subgoal @@ -33,11 +29,7 @@ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat + x3, x, x1, x4, x0 : nat ============================ (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> @@ -46,38 +38,26 @@ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat - H : forall x5 x6 : nat, - x5 + x1 = x4 + x6 -> - forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1) + x3, x, x1, x4, x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) H0 : x + x1 = x4 + x0 ============================ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat - H : forall x5 x6 : nat, - x5 + x1 = x4 + x6 -> - forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1) + x3, x, x1, x4, x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (Datatypes.S x + x1) H0 : x + x1 = x4 + x0 - x5 : nat - x6 : nat - x7 : nat - S : nat + x5, x6, x7, S : nat ============================ x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - a : nat - H : a = 0 -> forall a0 : nat, a0 = 0 + x3, a : nat + H : a = 0 -> forall a : nat, a = 0 ============================ a = 0 diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 66307236..60ee72b3 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -2,23 +2,21 @@ true ? 0; 1 : nat if true as x return (x ? nat; bool) then 0 else true : nat -Identifier 'proj1' now a keyword fun e : nat * nat => proj1 e : nat * nat -> nat -Identifier 'decomp' now a keyword decomp (true, true) as t, u in (t, u) : bool * bool -!(0 = 0) +! (0 = 0) : Prop forall n : nat, n = 0 : Prop -!(0 = 0) +! (0 = 0) : Prop -forall n : nat, #(n = n) +forall n : nat, # (n = n) : Prop -forall n n0 : nat, ##(n = n0) +forall n n0 : nat, ## (n = n0) : Prop -forall n n0 : nat, ###(n = n0) +forall n n0 : nat, ### (n = n0) : Prop 3 + 3 : Z @@ -28,21 +26,17 @@ forall n n0 : nat, ###(n = n0) : list nat (1; 2, 4) : nat * nat * nat -Identifier 'ifzero' now a keyword ifzero 3 : bool -Identifier 'pred' now a keyword pred 3 : nat fun n : nat => pred n : nat -> nat fun n : nat => pred n : nat -> nat -Identifier 'ifn' now a keyword -Identifier 'is' now a keyword fun x : nat => ifn x is succ n then n else 0 : nat -> nat -1- +1 - : bool -4 : Z @@ -50,14 +44,12 @@ The command has indeed failed with message: => Error: x should not be bound in a recursive pattern of the right-hand side. The command has indeed failed with message: => Error: in the right-hand side, y and z should appear in - term position as part of a recursive pattern. +term position as part of a recursive pattern. The command has indeed failed with message: => Error: The reference w was not found in the current environment. The command has indeed failed with message: -=> Error: x is unbound in the right-hand side. -The command has indeed failed with message: => Error: in the right-hand side, y and z should appear in - term position as part of a recursive pattern. +term position as part of a recursive pattern. The command has indeed failed with message: => Error: z is expected to occur in binding position in the right-hand side. The command has indeed failed with message: @@ -80,7 +72,6 @@ Nil : forall A : Type, list A NIL:list nat : list nat -Identifier 'I' now a keyword (false && I 3)%bool /\ I 6 : Prop [|1, 2, 3; 4, 5, 6|] @@ -89,11 +80,11 @@ Identifier 'I' now a keyword : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool)) fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z : (Z -> Z -> Z -> Z) -> Z -plus +Init.Nat.add : nat -> nat -> nat S : nat -> nat -mult +Init.Nat.mul : nat -> nat -> nat le : nat -> nat -> Prop @@ -101,7 +92,7 @@ plus : nat -> nat -> nat succ : nat -> nat -mult +Init.Nat.mul : nat -> nat -> nat le : nat -> nat -> Prop @@ -116,18 +107,24 @@ fun x : option Z => match x with end : option Z -> Z fun x : option Z => match x with - | SOME3 x0 => x0 - | NONE3 => 0 + | SOME2 x0 => x0 + | NONE2 => 0 end : option Z -> Z +fun x : list ?T1 => match x with + | NIL => NONE2 + | (_ :') t => SOME2 t + end + : list ?T1 -> option (list ?T1) +where +?T1 : [x : list ?T1 x1 : list ?T1 x0 := x1 : list ?T1 |- Type] (x, x1, + x0 cannot be used) s : s -Identifier 'foo' now a keyword 10 : nat fun _ : nat => 9 : nat -> nat -Identifier 'ONE' now a keyword fun (x : nat) (p : x = x) => match p with | ONE => ONE end = p diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 612b5325..adba688e 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -68,7 +68,7 @@ Coercion Zpos: nat >-> znat. Delimit Scope znat_scope with znat. Open Scope znat_scope. -Variable addz : znat -> znat -> znat. +Parameter addz : znat -> znat -> znat. Notation "z1 + z2" := (addz z1 z2) : znat_scope. (* Check that "3+3", where 3 is in nat and the coercion to znat is implicit, @@ -133,7 +133,8 @@ Fail Notation "( x , y , .. , z )" := (pair x (pair y z)). Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..). (* Right-unbound variable *) -Fail Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..). +(* Now allowed with an only parsing restriction *) +Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..). (* Not the right kind of recursive pattern *) Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)). @@ -244,7 +245,11 @@ Check (fun x => match x with SOME2 x => x | NONE2 => 0 end). Notation NONE3 := @None. Notation SOME3 := @Some. -Check (fun x => match x with SOME3 x => x | NONE3 => 0 end). +Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end). + +Notation "a :'" := (cons a) (at level 12). + +Check (fun x => match x with | nil => NONE | h :' t => SOME3 _ t end). (* Check correct matching of "Type" in notations. Of course the notation denotes a term that will be reinterpreted with a different @@ -275,3 +280,4 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p. Notation "1" := eq_refl. Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p. + diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index cf45025e..58ec1de5 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -1,6 +1,6 @@ 2 3 : PAIR -2[+]3 +2 [+] 3 : nat forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x : Prop @@ -10,7 +10,7 @@ end : nat let '(a, _, _) := (2, 3, 4) in a : nat -exists myx (y : bool), myx = y +exists myx y : bool, myx = y : Prop fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 : (nat -> nat -> Prop) -> nat -> Prop @@ -24,7 +24,6 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop -Identifier 'λ' now a keyword λ n p : nat, n + p = 0 : nat -> nat -> Prop λ (A : Type) (n p : A), n = p @@ -33,12 +32,11 @@ Identifier 'λ' now a keyword : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -Identifier 'let'' now a keyword let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat -Notation plus2 n := (S (S n)) +Notation plus2 n := (S(S(n))) λ n : list(nat), match n with | nil => 2 diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 23f33081..08df9150 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -2,6 +2,11 @@ Axioms: foo : nat Axioms: foo : nat +Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZAdd +Fetching opaque proofs from disk for Coq.Arith.PeanoNat +Fetching opaque proofs from disk for Coq.Classes.Morphisms +Fetching opaque proofs from disk for Coq.Init.Logic +Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZBase Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 598bb728..0457c860 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,16 +1,17 @@ -existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P +existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} +existT is template universe polymorphic Argument A is implicit Argument scopes are [type_scope _ _ _] Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := - existT : forall x : A, P x -> sigT P + existT : forall x : A, P x -> {x : A & P x} For sigT: Argument A is implicit For existT: Argument A is implicit For sigT: Argument scopes are [type_scope type_scope] For existT: Argument scopes are [type_scope _ _ _] -existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P +existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x @@ -24,6 +25,7 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x +eq_refl is not universe polymorphic When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: @@ -36,28 +38,30 @@ When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: Argument A is implicit -plus = -fix plus (n m : nat) {struct n} : nat := +Nat.add = +fix add (n m : nat) {struct n} : nat := match n with | 0 => m - | S p => S (plus p m) + | S p => S (add p m) end : nat -> nat -> nat +Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] -plus : nat -> nat -> nat +Nat.add : nat -> nat -> nat +Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] -plus is transparent -Expands to: Constant Coq.Init.Peano.plus -plus : nat -> nat -> nat +Nat.add is transparent +Expands to: Constant Coq.Init.Nat.add +Nat.add : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 +plus_n_O is not universe polymorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O -Warning: Implicit Arguments is deprecated; use Arguments instead Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m @@ -76,12 +80,13 @@ For le_n: Argument scope is [nat_scope] For le_S: Argument scopes are [nat_scope nat_scope _] comparison : Set +comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison -Warning: Implicit Arguments is deprecated; use Arguments instead bar : foo +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -89,12 +94,14 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted bar : foo +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -102,6 +109,7 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -109,7 +117,6 @@ Argument x is implicit and maximally inserted Module Coq.Init.Peano Notation existS2 := existT2 Expands to: Notation Coq.Init.Specif.existS2 -Warning: Implicit Arguments is deprecated; use Arguments instead Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted @@ -128,3 +135,15 @@ For eq_refl, when applied to 1 argument: Argument A is implicit and maximally inserted For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] +n:nat + +Hypothesis of the goal context. +h:(n <> newdef n) + +Hypothesis of the goal context. +g:(nat -> nat) + +Constant (let in) of the goal context. +h:(n <> newdef n) + +Hypothesis of the goal context. diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index deeb1f65..3c623346 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -6,9 +6,9 @@ Print eq_refl. About eq_refl. Print Implicit eq_refl. -Print plus. -About plus. -Print Implicit plus. +Print Nat.add. +About Nat.add. +Print Implicit Nat.add. About plus_n_O. @@ -39,3 +39,19 @@ Print eq_refl. Arguments eq_refl {A} {x}, {A} x. (* Test new syntax *) Print eq_refl. + + +Definition newdef := fun x:nat => x. + +Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. + intros n h h'. + About n. (* search hypothesis *) + About h. (* search hypothesis *) +Abort. + +Goal forall n:nat, let g := newdef in n <> newdef n -> newdef n <> n -> False. + intros n g h h'. + About g. (* search hypothesis *) + About h. (* search hypothesis *) +Abort. + diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 5d8f98ed..c17b285b 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,24 +1,108 @@ -le_S: forall n m : nat, n <= m -> n <= S m le_n: forall n : nat, n <= n -le_pred: forall n m : nat, n <= m -> pred n <= pred m +le_S: forall n m : nat, n <= m -> n <= S m +le_ind: + forall (n : nat) (P : nat -> Prop), + P n -> + (forall m : nat, n <= m -> P m -> P (S m)) -> + forall n0 : nat, n <= n0 -> P n0 +le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m le_S_n: forall n m : nat, S n <= S m -> n <= m -false: bool +le_0_n: forall n : nat, 0 <= n +le_n_S: forall n m : nat, n <= m -> S n <= S m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m true: bool -xorb: bool -> bool -> bool +false: bool +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b +bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b +andb: bool -> bool -> bool orb: bool -> bool -> bool -negb: bool -> bool implb: bool -> bool -> bool -andb: bool -> bool -> bool -pred_Sn: forall n : nat, n = pred (S n) -plus_n_Sm: forall n m : nat, S (n + m) = n + S m +xorb: bool -> bool -> bool +negb: bool -> bool +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +eq_true: bool -> Prop +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b +eq_true_rec: + forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b +is_true: bool -> Prop +eq_true_ind_r: + forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true +eq_true_rec_r: + forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_rect_r: + forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true +BoolSpec: Prop -> Prop -> bool -> Prop +BoolSpec_ind: + forall (P Q : Prop) (P0 : bool -> Prop), + (P -> P0 true) -> + (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b +Nat.eqb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +Nat.testbit: nat -> nat -> bool +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +bool_choice: + forall (S : Set) (R1 R2 : S -> Prop), + (forall x : S, {R1 x} + {R2 x}) -> + {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +eq_S: forall x y : nat, x = y -> S x = S y +f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +pred_Sn: forall n : nat, n = Nat.pred (S n) +eq_add_S: forall n m : nat, S n = S m -> n = m +not_eq_S: forall n m : nat, n <> m -> S n <> S m +O_S: forall n : nat, 0 <> S n +n_Sn: forall n : nat, n <> S n +f_equal2_plus: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +f_equal2_nat: + forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), + x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 plus_n_O: forall n : nat, n = n + 0 -plus_Sn_m: forall n m : nat, S n + m = S (n + m) plus_O_n: forall n : nat, 0 + n = n -mult_n_Sm: forall n m : nat, n * m + n = n * S m +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +plus_Sn_m: forall n m : nat, S n + m = S (n + m) +f_equal2_mult: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 mult_n_O: forall n : nat, 0 = n * 0 -min_r: forall n m : nat, m <= n -> min n m = m -min_l: forall n m : nat, n <= m -> min n m = n -max_r: forall n m : nat, n <= m -> max n m = m -max_l: forall n m : nat, m <= n -> max n m = n -eq_add_S: forall n m : nat, S n = S m -> n = m -eq_S: forall x y : nat, x = y -> S x = S y +mult_n_Sm: forall n m : nat, n * m + n = n * S m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +bool_choice: + forall (S : Set) (R1 R2 : S -> Prop), + (forall x : S, {R1 x} + {R2 x}) -> + {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +h': newdef n <> n +h: n <> newdef n +h': newdef n <> n +h: n <> newdef n +h: n <> newdef n +h: n <> newdef n +h': ~ P n +h: P n +h': ~ P n +h: P n +h': ~ P n +h: P n +h: P n +h: P n diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index f1489f22..2a0f0b40 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -3,3 +3,27 @@ Search le. (* app nodes *) Search bool. (* no apps *) Search (@eq nat). (* complex pattern *) +Search (@eq _ _ true). +Search (@eq _ _ _) true -false. (* andb_prop *) +Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *) + +Definition newdef := fun x:nat => x. + +Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. + intros n h h'. + Search n. (* search hypothesis *) + Search newdef. (* search hypothesis *) + Search ( _ <> newdef _). (* search hypothesis, pattern *) + Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *) +Abort. + +Goal forall n (P:nat -> Prop), P n -> ~P n -> False. + intros n P h h'. + Search P. (* search hypothesis also for patterns *) + Search (P _). (* search hypothesis also for patterns *) + Search (P n). (* search hypothesis also for patterns *) + Search (P _) -"h'". (* search hypothesis also for patterns *) + Search (P _) -not. (* search hypothesis also for patterns *) + +Abort. + diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out new file mode 100644 index 00000000..0d5924ec --- /dev/null +++ b/test-suite/output/SearchHead.out @@ -0,0 +1,39 @@ +le_n: forall n : nat, n <= n +le_S: forall n m : nat, n <= m -> n <= S m +le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m +le_S_n: forall n m : nat, S n <= S m -> n <= m +le_0_n: forall n : nat, 0 <= n +le_n_S: forall n m : nat, n <= m -> S n <= S m +true: bool +false: bool +andb: bool -> bool -> bool +orb: bool -> bool -> bool +implb: bool -> bool -> bool +xorb: bool -> bool -> bool +negb: bool -> bool +Nat.eqb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +Nat.testbit: nat -> nat -> bool +eq_S: forall x y : nat, x = y -> S x = S y +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +pred_Sn: forall n : nat, n = Nat.pred (S n) +eq_add_S: forall n m : nat, S n = S m -> n = m +f_equal2_plus: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +plus_n_O: forall n : nat, n = n + 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +plus_Sn_m: forall n m : nat, S n + m = S (n + m) +f_equal2_mult: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 +mult_n_O: forall n : nat, 0 = n * 0 +mult_n_Sm: forall n m : nat, n * m + n = n * S m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m +h: newdef n +h: P n diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v new file mode 100644 index 00000000..2ee8a0d1 --- /dev/null +++ b/test-suite/output/SearchHead.v @@ -0,0 +1,19 @@ +(* Some tests of the Search command *) + +SearchHead le. (* app nodes *) +SearchHead bool. (* no apps *) +SearchHead (@eq nat). (* complex pattern *) + +Definition newdef := fun x:nat => x = x. + +Goal forall n:nat, newdef n -> False. + intros n h. + SearchHead newdef. (* search hypothesis *) +Abort. + + +Goal forall n (P:nat -> Prop), P n -> False. + intros n P h. + SearchHead P. (* search hypothesis also for patterns *) +Abort. + diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 9106a4e3..1eb7eca8 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -1,30 +1,83 @@ -false: bool true: bool -xorb: bool -> bool -> bool +false: bool +andb: bool -> bool -> bool orb: bool -> bool -> bool -negb: bool -> bool implb: bool -> bool -> bool -andb: bool -> bool -> bool -S: nat -> nat +xorb: bool -> bool -> bool +negb: bool -> bool +Nat.eqb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +Nat.testbit: nat -> nat -> bool O: nat -pred: nat -> nat -plus: nat -> nat -> nat -mult: nat -> nat -> nat -minus: nat -> nat -> nat -min: nat -> nat -> nat -max: nat -> nat -> nat +S: nat -> nat length: forall A : Type, list A -> nat +Nat.zero: nat +Nat.one: nat +Nat.two: nat +Nat.succ: nat -> nat +Nat.pred: nat -> nat +Nat.add: nat -> nat -> nat +Nat.double: nat -> nat +Nat.mul: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.max: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.div: nat -> nat -> nat +Nat.modulo: nat -> nat -> nat +Nat.gcd: nat -> nat -> nat +Nat.square: nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat +Nat.sqrt: nat -> nat +Nat.log2_iter: nat -> nat -> nat -> nat -> nat +Nat.log2: nat -> nat +Nat.div2: nat -> nat +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +Nat.land: nat -> nat -> nat +Nat.lor: nat -> nat -> nat +Nat.ldiff: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat + S: nat -> nat -pred: nat -> nat -plus: nat -> nat -> nat -mult: nat -> nat -> nat -minus: nat -> nat -> nat -min: nat -> nat -> nat -max: nat -> nat -> nat +Nat.succ: nat -> nat +Nat.pred: nat -> nat +Nat.add: nat -> nat -> nat +Nat.double: nat -> nat +Nat.mul: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.max: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.div: nat -> nat -> nat +Nat.modulo: nat -> nat -> nat +Nat.gcd: nat -> nat -> nat +Nat.square: nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat +Nat.sqrt: nat -> nat +Nat.log2_iter: nat -> nat -> nat -> nat -> nat +Nat.log2: nat -> nat +Nat.div2: nat -> nat +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +Nat.land: nat -> nat -> nat +Nat.lor: nat -> nat -> nat +Nat.ldiff: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat mult_n_Sm: forall n m : nat, n * m + n = n * S m -le_n: forall n : nat, n <= n identity_refl: forall (A : Type) (a : A), identity a a -eq_refl: forall (A : Type) (x : A), x = x iff_refl: forall A : Prop, A <-> A +eq_refl: forall (A : Type) (x : A), x = x +Nat.divmod: nat -> nat -> nat -> nat -> nat * nat +le_n: forall n : nat, n <= n pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B +Nat.divmod: nat -> nat -> nat -> nat -> nat * nat + +h: n <> newdef n +h: n <> newdef n +h: P n +h': ~ P n +h: P n +h: P n diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v index 802d8c97..bde195a5 100644 --- a/test-suite/output/SearchPattern.v +++ b/test-suite/output/SearchPattern.v @@ -17,3 +17,20 @@ SearchPattern (forall (x:?A) (y:?B), _ ?A ?B). (* No delta-reduction *) SearchPattern (Exc _). + +Definition newdef := fun x:nat => x. + +Goal forall n:nat, n <> newdef n -> False. + intros n h. + SearchPattern ( _ <> newdef _). (* search hypothesis *) + SearchPattern ( n <> newdef _). (* search hypothesis *) +Abort. + +Goal forall n (P:nat -> Prop), P n -> ~P n -> False. + intros n P h h'. + SearchPattern (P _). (* search hypothesis also for patterns *) + Search (~P n). (* search hypothesis also for patterns *) + Search (P _) -"h'". (* search hypothesis also for patterns *) + Search (P _) -not. (* search hypothesis also for patterns *) + +Abort.
\ No newline at end of file diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out index f87aea1c..5edea5df 100644 --- a/test-suite/output/SearchRewrite.out +++ b/test-suite/output/SearchRewrite.out @@ -1,2 +1,5 @@ plus_n_O: forall n : nat, n = n + 0 plus_O_n: forall n : nat, 0 + n = n +h: n = newdef n +h: n = newdef n +h: n = newdef n diff --git a/test-suite/output/SearchRewrite.v b/test-suite/output/SearchRewrite.v index 171a7363..53d043c6 100644 --- a/test-suite/output/SearchRewrite.v +++ b/test-suite/output/SearchRewrite.v @@ -2,3 +2,12 @@ SearchRewrite (_+0). (* left *) SearchRewrite (0+_). (* right *) + +Definition newdef := fun x:nat => x. + +Goal forall n:nat, n = newdef n -> False. + intros n h. + SearchRewrite (newdef _). + SearchRewrite n. (* use hypothesis for patterns *) + SearchRewrite (newdef n). (* use hypothesis for patterns *) +Abort. diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index f94ed642..67b65d4b 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,7 +1,15 @@ TrM.A = M.A : Set + +TrM.A is not universe polymorphic OpM.A = M.A : Set + +OpM.A is not universe polymorphic TrM.B = M.B : Set + +TrM.B is not universe polymorphic *** [ OpM.B : Set ] + +OpM.B is not universe polymorphic diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 4f8de1dc..d69baaec 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -4,7 +4,17 @@ fun e : option L => match e with | None => None end : option L -> option L -fun n : nat => let x := A n in ?12 ?15:T n + +P is not universe polymorphic +fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H + : forall m n p : nat, S m <= S n + p -> m <= n + p +fun n : nat => let x := A n in ?y ?y0:T n : forall n : nat, T n -fun n : nat => ?20 ?23:T n +where +?y : [n : nat x := A n : T n |- ?T0 -> T n] +?y0 : [n : nat x := A n : T n |- ?T0] +fun n : nat => ?y ?y0:T n : forall n : nat, T n +where +?y : [n : nat |- ?T0 -> T n] +?y0 : [n : nat |- ?T0] diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 2b564f48..cd9a4a12 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -13,6 +13,10 @@ Definition P (e:option L) := Print P. +(* Check that plus is folded even if reduction is involved *) +Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H). + + (* Check that the heuristic to solve constraints is not artificially dependent on the presence of a let-in, and in particular that the second [_] below is not inferred to be n, as if obtained by diff --git a/test-suite/output/names.out b/test-suite/output/names.out new file mode 100644 index 00000000..2892dfd5 --- /dev/null +++ b/test-suite/output/names.out @@ -0,0 +1,6 @@ +The command has indeed failed with message: +=> Error: +In environment +y : nat +The term "a y" has type "{y0 : nat | y = y0}" +while it is expected to have type "{x : nat | x = y}". diff --git a/test-suite/output/names.v b/test-suite/output/names.v new file mode 100644 index 00000000..b3b5071a --- /dev/null +++ b/test-suite/output/names.v @@ -0,0 +1,5 @@ +(* Test no clash names occur *) +(* see bug #2723 *) + +Parameter a : forall x, {y:nat|x=y}. +Fail Definition b y : {x:nat|x=y} := a y. diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v index c4592369..ab626282 100644 --- a/test-suite/output/reduction.v +++ b/test-suite/output/reduction.v @@ -1,6 +1,6 @@ (* Test the behaviour of hnf and simpl introduced in revision *) -Variable n:nat. +Parameter n:nat. Definition a:=0. Eval simpl in (fix plus (n m : nat) {struct n} : nat := diff --git a/test-suite/output/set.out b/test-suite/output/set.out index 333fbb86..4dfd2bc2 100644 --- a/test-suite/output/set.out +++ b/test-suite/output/set.out @@ -6,16 +6,13 @@ x = x 1 subgoal - y1 := 0 : nat - y2 := 0 : nat + y1, y2 := 0 : nat x := y2 + 0 : nat ============================ x = x 1 subgoal - y1 := 0 : nat - y2 := 0 : nat - y3 := 0 : nat + y1, y2, y3 := 0 : nat x := y2 + y3 : nat ============================ x = x diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v index 5f1926f1..89638eed 100644 --- a/test-suite/output/simpl.v +++ b/test-suite/output/simpl.v @@ -4,10 +4,10 @@ Goal forall x, 0+x = 1+x. intro x. simpl (_ + x). Show. -Undo. +Undo 2. simpl (_ + x) at 2. Show. -Undo. +Undo 2. simpl (0 + _). Show. -Undo. +Undo 2. |