From 71d71554b7b3b0e50f67d5d1c4428c1ec4e6fa44 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Apr 2017 15:48:07 +0200 Subject: 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. --- kernel/cClosure.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/cClosure.ml') 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. *) -- cgit v1.2.3