diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-17 15:07:39 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-17 15:07:39 +0200 |
| commit | eba5d64fee0bf6235265f1f6cc884b4cbefe2704 (patch) | |
| tree | 9c8950e67e27c3d781bc1d69a0d4066eadd845b5 /kernel/term_typing.ml | |
| parent | c707b52613d650cac665aaf252a449ab25ce9351 (diff) | |
| parent | 839e87fffdf2634b841aeba6de6d36a2d7a27dbd (diff) | |
Merge PR #783: Remove some useless code in Term_typing
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3e516cae0..cf82d54ec 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -265,11 +265,8 @@ let infer_declaration ~trust env kn dcl = let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in unzip ectx j in - let subst = Univ.LMap.empty in let _ = judge_of_cast env j DEFAULTcast tyj in - assert (eq_constr typ tyj.utj_val); let c = hcons_constr j.uj_val in - let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in @@ -299,7 +296,6 @@ let infer_declaration ~trust env kn dcl = | Some t -> let tj = infer_type env t in let _ = judge_of_cast env j DEFAULTcast tj in - assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr usubst t) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in |