diff options
Diffstat (limited to 'checker/environ.ml')
| -rw-r--r-- | checker/environ.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index d960e2a7c..d79cb118b 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -124,10 +124,10 @@ exception NotEvaluableConst of const_evaluation_result let constant_value env kn = let cb = lookup_constant kn env in - if cb.const_opaque then raise (NotEvaluableConst Opaque); match cb.const_body with - | Some l_body -> force_constr l_body - | None -> raise (NotEvaluableConst NoBody) + | Def l_body -> force_constr l_body + | OpaqueDef _ -> raise (NotEvaluableConst Opaque) + | Undef _ -> raise (NotEvaluableConst NoBody) (* A global const is evaluable if it is defined and not opaque *) let evaluable_constant cst env = |