diff options
| author | Gaëtan Gilbert | 2020-02-06 17:43:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | ebd1c087298a50f85d3f227452b8a3d1fb7a625c (patch) | |
| tree | f5fc856b3b8963e27fdc782472bdcde5f2a6b1bb /proofs/logic.ml | |
| parent | 48b142d0e915e946274c14ab354f174cc5b6df51 (diff) | |
unsafe_type_of -> type_of in Logic.check_typability
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index a361c4208e..bac13fcfc3 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -79,7 +79,7 @@ let check = ref false let with_check = Flags.with_option check let check_typability env sigma c = - if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in () + if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma (************************************************************************) (************************************************************************) @@ -363,7 +363,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> - check_typability env sigma ty; + let sigma = check_typability env sigma ty in let sigma = check_conv_leq_goal env sigma trm ty conclty in let res = mk_refgoals sigma goal goalacc ty t in (* we keep the casts (in particular VMcast and NATIVEcast) except @@ -430,13 +430,13 @@ and mk_hdgoals sigma goal goalacc trm = Goal.V82.mk_goal sigma hyps concl in match kind trm with | Cast (c,_, ty) when isMeta c -> - check_typability env sigma ty; + let sigma = check_typability env sigma ty in let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> - check_typability env sigma ty; + let sigma = check_typability env sigma ty in mk_refgoals sigma goal goalacc ty t | App (f,l) -> |