From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 pretyping/cbv.mli | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'pretyping/cbv.mli')

diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 9ab15886..de66d22b 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cbv.mli 11897 2009-02-09 19:28:02Z barras $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -29,18 +29,20 @@ val cbv_norm         : cbv_infos -> constr -> constr
 (*i This is for cbv debug *)
 type cbv_value =
   | VAL of int * constr
+  | STACK of int * cbv_value * cbv_stack
+  | CBN of constr * cbv_value subs
   | LAM of int * (name * constr) list * constr * cbv_value subs
   | FIXP of fixpoint * cbv_value subs * cbv_value array
   | COFIXP of cofixpoint * cbv_value subs * cbv_value array
   | CONSTR of constructor * cbv_value array
 
-val shift_value : int -> cbv_value -> cbv_value
-
-type cbv_stack =
+and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
   | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
 
+val shift_value : int -> cbv_value -> cbv_value
+
 val stack_app : cbv_value array -> cbv_stack -> cbv_stack
 val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
 
-- 
cgit v1.2.3