diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 4 | ||||
| -rw-r--r-- | kernel/names.ml | 8 | ||||
| -rw-r--r-- | kernel/names.mli | 3 |
3 files changed, 11 insertions, 4 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. *) diff --git a/kernel/names.ml b/kernel/names.ml index afdbe0c0dc..ae34033355 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -104,8 +104,12 @@ struct | _ -> false let hash = function - | Anonymous -> 0 - | Name id -> Id.hash id + | Anonymous -> 0 + | Name id -> Id.hash id + + let print = function + | Anonymous -> str "_" + | Name id -> Id.print id module Self_Hashcons = struct diff --git a/kernel/names.mli b/kernel/names.mli index 5b0163aa55..c73eb197bb 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -105,6 +105,9 @@ sig val hcons : t -> t (** Hashconsing over names. *) + val print : t -> Pp.std_ppcmds + (** Pretty-printer (print "_" for [Anonymous]. *) + end (** {6 Type aliases} *) |