Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v
new file mode 100644
index 00000000..4a460a83
--- /dev/null
+++ b/test-suite/output/reduction.v
@@ -0,0 +1,13 @@
+(* Test the behaviour of hnf and simpl introduced in revision *)
+
+Variable n:nat.
+Definition a:=0.
+
+Eval simpl in (fix plus (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (p + m)
+  end) a a.
+
+Eval hnf in match (plus (S n) O) with S n => n | _ => O end.  
+