diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 15:31:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 15:35:59 +0200 |
| commit | 0cebd2b86a90cc1361bcfac6bb097540e22c9a21 (patch) | |
| tree | 648ece59fd72185da10d71771d9f858aa1fa7fd4 /test-suite/output/ArgumentsScope.out | |
| parent | 6a3767e48e91604071b5709a6658aa2f255a4522 (diff) | |
Fixing output test-suite: since universe polymorphism, the Print command
shows the polymorphism status of the term.
Diffstat (limited to 'test-suite/output/ArgumentsScope.out')
| -rw-r--r-- | test-suite/output/ArgumentsScope.out | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 6643c1429..358a96bc3 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,56 +1,70 @@ a : bool -> bool +a is monomorphic Argument scope is [bool_scope] Expands to: Variable a b : bool -> bool +b is monomorphic Argument scope is [bool_scope] Expands to: Variable b negb'' : bool -> bool +negb'' is monomorphic Argument scope is [bool_scope] negb'' is transparent Expands to: Constant Top.A.B.negb'' negb' : bool -> bool +negb' is monomorphic Argument scope is [bool_scope] negb' is transparent Expands to: Constant Top.A.negb' negb : bool -> bool +negb is monomorphic Argument scope is [bool_scope] negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool +a is monomorphic Expands to: Variable a b : bool -> bool +b is monomorphic Expands to: Variable b negb : bool -> bool +negb is monomorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool +negb' is monomorphic negb' is transparent Expands to: Constant Top.A.negb' negb'' : bool -> bool +negb'' is monomorphic negb'' is transparent Expands to: Constant Top.A.B.negb'' a : bool -> bool +a is monomorphic Expands to: Variable a negb : bool -> bool +negb is monomorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool +negb' is monomorphic negb' is transparent Expands to: Constant Top.negb' negb'' : bool -> bool +negb'' is monomorphic negb'' is transparent Expands to: Constant Top.negb'' |