From 848f2c41e605287c99e84c2f8ea1747c8a34e201 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 3 Jun 2014 18:07:18 +0200
Subject: 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.
---
 test-suite/output/Arguments.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite/output/Arguments.v')

diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 573cfdab22..4d4ab54f14 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 }.
-- 
cgit v1.2.3