diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-11 15:48:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-12 13:59:31 +0200 |
| commit | 71d71554b7b3b0e50f67d5d1c4428c1ec4e6fa44 (patch) | |
| tree | f4952c708dab98506f2d6b44d3123ebba9b42dac /kernel/cClosure.ml | |
| parent | f41944730792070d4a3074aa1fe1f8465062b758 (diff) | |
Missing optimization when Kernel Term Sharing is disabled.
We don't have to perfom in-place updates because we actually know that there
is none on the stack. This should speed up UniMath.
Diffstat (limited to 'kernel/cClosure.ml')
| -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 b1dd26119..8515d51b0 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. *) |