diff options
| author | barras | 2001-09-05 13:19:12 +0000 |
|---|---|---|
| committer | barras | 2001-09-05 13:19:12 +0000 |
| commit | 2fac2137bf72662bad76d9baa54611bec8a4143a (patch) | |
| tree | c04c056e44d2eb065d51f3ea69238d9054106c0e /kernel/closure.mli | |
| parent | 15d975fb59e146f15eeef7279cc63354c0276f2e (diff) | |
Version de la reduction dans Closure plus econome en memoire:
- la pile ne contient plus les arguments appliques deja consommes
- ajout d'un "lock" sur les glacons en cours de calcul
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1922 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 6f5afc4e27..e755f28d98 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -134,7 +134,7 @@ val create: one by one *) type 'a stack_member = - | Zapp of 'a array * int + | Zapp of 'a list | Zcase of case_info * 'a * 'a array | Zfix of 'a * 'a stack | Zshift of int @@ -182,6 +182,7 @@ type fterm = | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs + | FLOCKED and freference = | FConst of section_path * fconstr array |