diff options
Diffstat (limited to 'test-suite/output/PrintInfos.out')
| -rw-r--r-- | test-suite/output/PrintInfos.out | 45 |
1 files changed, 32 insertions, 13 deletions
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. |