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.
---
 pretyping/reductionops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 8739731983..548517dbf7 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -55,6 +55,8 @@ module Stack : sig
   | Case of case_info * 'a * 'a array * 'a Cst_stack.t
   | Proj of int * int * projection
   | Fix of fixpoint * 'a t * 'a Cst_stack.t
+  | Cst of pconstant * int (** current foccussed arg *) * int list (** remaining args *)
+    * 'a t * 'a Cst_stack.t
   | Shift of int
   | Update of 'a
   and 'a t = 'a member list
-- 
cgit v1.2.3