diff options
| author | Maxime Dénès | 2017-05-29 14:43:01 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-29 14:43:01 +0200 |
| commit | 1e93bc46bf8bbfe839bba39c18f7617d9f5caa5b (patch) | |
| tree | 5a717dab2534a97df47956ebdaadca62514c3f3b /kernel | |
| parent | 4c1260299b707bd27765b0ab365092046b134a69 (diff) | |
| parent | 71d71554b7b3b0e50f67d5d1c4428c1ec4e6fa44 (diff) | |
Merge PR#555: Missing optimization when Kernel Term Sharing is disabled.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index b1dd26119e..8515d51b0d 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1000,7 +1000,7 @@ let rec kl info m = if is_val m then (incr prune; term_of_fconstr m) else let (nm,s) = kni info m [] in - let _ = fapp_stack(nm,s) in (* to unlock Zupdates! *) + let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) zip_term (kl info) (norm_head info nm) s (* no redex: go up for atoms and already normalized terms, go down @@ -1050,7 +1050,7 @@ let inject c = mk_clos (subs_id 0) c let whd_stack infos m stk = let k = kni infos m stk in - let _ = fapp_stack k in (* to unlock Zupdates! *) + let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k (* cache of constants: the body is computed only when needed. *) |