summaryrefslogtreecommitdiff
path: root/checker/environ.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/environ.ml')
-rw-r--r--checker/environ.ml17
1 files changed, 4 insertions, 13 deletions
diff --git a/checker/environ.ml b/checker/environ.ml
index f7dd46f8..99b36457 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -98,7 +98,7 @@ let named_type id env =
(* Universe constraints *)
let add_constraints c env =
- if c == Constraint.empty then
+ if c == empty_constraint then
env
else
let s = env.env_stratification in
@@ -121,25 +121,16 @@ let add_constant kn cs env =
env_constants = new_constants } in
{ env with env_globals = new_globals }
-(* constant_type gives the type of a constant *)
-let constant_type env kn =
- let cb = lookup_constant kn env in
- cb.const_type
-
type const_evaluation_result = NoBody | Opaque
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)
-
-let constant_opt_value env cst =
- try Some (constant_value env cst)
- with NotEvaluableConst _ -> None
+ | 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 =