Skip to content

Commit

Permalink
Tweak a weird syntax in CClosure.
Browse files Browse the repository at this point in the history
The way it was written made it look as if some part of the code was evaluated
for side-effects, and that there had been a merge conflict somehow. We rephrase
the check in a probably more efficient way.
  • Loading branch information
ppedrot committed May 22, 2024
1 parent 86562aa commit 71ad4d6
Showing 1 changed file with 6 additions and 7 deletions.
13 changes: 6 additions & 7 deletions kernel/cClosure.ml
Original file line number Diff line number Diff line change
Expand Up @@ -399,14 +399,13 @@ end = struct
let cb = lookup_constant cst env in
shortcut_irrelevant info (UVars.subst_instance_relevance u cb.const_relevance);
let ts = RedFlags.red_transparent info.i_flags in
if TransparentState.is_transparent_constant ts cst then begin
match Cmap_env.find_opt cst env.symb_pats with
| Some r ->
let b = match [@ocaml.warning "-4"] cb.const_body with Symbol b -> b | _ -> assert false in
raise (NotEvaluableConst (HasRules (u, b, r)))
| None -> ();
if TransparentState.is_transparent_constant ts cst then match cb.const_body with
| Undef _ | Def _ | OpaqueDef _ | Primitive _ ->
Def (constant_value_in u cb.const_body)
end else
| Symbol b ->
let r = Cmap_env.get cst env.symb_pats in
raise (NotEvaluableConst (HasRules (u, b, r)))
else
raise Not_found
with
| Irrelevant -> Def mk_irrelevant
Expand Down

0 comments on commit 71ad4d6

Please sign in to comment.