diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-08-18 09:26:03 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-08-18 09:26:03 +0000 |
| commit | a9cab41ba380e1e5ab2c4d18880a73dbafbd914b (patch) | |
| tree | 2a3d95f84dd4d14c0332ce899ffdb97190f1a262 /kernel/closure.ml | |
| parent | 9eabd9dce9f6541099394f0492aeb669a1005ee9 (diff) | |
module Reduction (debut)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index a543f486c..fa174d610 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -849,12 +849,14 @@ let search_frozen_cst info op vars = (* cache of constants: the body is computed only when needed. *) type 'a clos_infos = (fconstr, 'a) infos -let create_clos_infos flgs sigma = +let create_clos_infos flgs env = { i_flags = flgs; i_repr = (fun old_info c -> inject c); - i_env = sigma; + i_env = env; i_tab = Hashtbl.create 17 } +let clos_infos_env infos = infos.i_env + (* Head normal form. *) let fhnf info v = let uv = unfreeze info v in |