diff options
Diffstat (limited to 'test-suite/output/PrintInfos.out')
| -rw-r--r-- | test-suite/output/PrintInfos.out | 34 |
1 files changed, 2 insertions, 32 deletions
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index ba076f05..1307a8f2 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -2,7 +2,7 @@ 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 _ _ _] +Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} @@ -10,7 +10,7 @@ Inductive sigT (A : Type) (P : A -> Type) : Type := 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 _ _ _] +For existT: Argument scopes are [type_scope function_scope _ _] existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit @@ -66,14 +66,6 @@ For le_S: Argument n is implicit and maximally inserted For le: Argument scopes are [nat_scope nat_scope] For le_n: Argument scope is [nat_scope] For le_S: Argument scopes are [nat_scope nat_scope _] -Inductive le (n : nat) : nat -> Prop := - le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m - -For le_S: Argument m is implicit -For le_S: Argument n is implicit and maximally inserted -For le: Argument scopes are [nat_scope nat_scope] -For le_n: Argument scope is [nat_scope] -For le_S: Argument scopes are [nat_scope nat_scope _] comparison : Set Expands to: Inductive Coq.Init.Datatypes.comparison @@ -92,19 +84,6 @@ Expanded type for implicit arguments bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted -bar : foo - -Expanded type for implicit arguments -bar : forall x : nat, x = 0 - -Argument x is implicit and maximally inserted -Expands to: Constant Top.bar -*** [ bar : foo ] - -Expanded type for implicit arguments -bar : forall x : nat, x = 0 - -Argument x is implicit and maximally inserted Module Coq.Init.Peano Notation existS2 := existT2 Expands to: Notation Coq.Init.Specif.existS2 @@ -117,15 +96,6 @@ 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 _] -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x - -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments A, x are implicit and maximally inserted -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. |