diff options
| author | Pierre-Marie Pédrot | 2018-03-27 16:16:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-26 13:50:10 +0200 |
| commit | de20a45db5d45154819f2ed4359effdbb8bf0292 (patch) | |
| tree | 4df0add753c3464868f3bc61350cdd9ff7dc445a /pretyping/cbv.ml | |
| parent | 09c76adaff7adaada1c49479dfa9a4d0a4b416af (diff) | |
Turn the kernel reduction sharing flag into an argument passed in the cache.
We move the global declaration of that argument to the environment, and reuse
the Global module to handle this flag.
Note that the checker was not using this flag before this patch, and still
doesn't use it. This should probably be fixed in a later patch.
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index da6e26cc4b..fc24e9b3a9 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -455,7 +455,8 @@ let cbv_norm infos constr = (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = let infos = create - (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) + ~share:true (** Not used by cbv *) + ~repr:(fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) flgs env (Reductionops.safe_evar_value sigma) in |