diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-06-03 18:07:18 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-06-04 14:11:33 +0200 |
| commit | 848f2c41e605287c99e84c2f8ea1747c8a34e201 (patch) | |
| tree | 5454e67be508c8dea44db6069455cdcf41dd5ead /test-suite/output/Arguments.v | |
| parent | 7d7784230d91f67bdc5a3bf06caab296c64034a8 (diff) | |
cbn understand ! Arguments directive
Of course, this is an under approximation of the expected behavior : unfolding
a constant iff a leaf of its underlying split-tree is reached.
Diffstat (limited to 'test-suite/output/Arguments.v')
| -rw-r--r-- | test-suite/output/Arguments.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 573cfdab2..4d4ab54f1 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -36,6 +36,8 @@ 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 }. |