diff options
| author | Pierre Boutillier | 2014-06-03 18:07:18 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-06-04 14:11:33 +0200 |
| commit | 848f2c41e605287c99e84c2f8ea1747c8a34e201 (patch) | |
| tree | 5454e67be508c8dea44db6069455cdcf41dd5ead /pretyping/reductionops.mli | |
| 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 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 |