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/type_errors.ml | |
| 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/type_errors.ml')
0 files changed, 0 insertions, 0 deletions