diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-06-13 22:16:46 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-06-13 22:25:36 +0200 |
| commit | 839e87fffdf2634b841aeba6de6d36a2d7a27dbd (patch) | |
| tree | 1303c6797704aa98c38bc140c7ff9bc44b404cfe /kernel/term_typing.ml | |
| parent | 25462addaf604ff51e886bbc92937bb272982b04 (diff) | |
Remove some useless code in Term_typing
The [let _typ = ...] comes from before universe polymorphism. In those
times it was [let _typ, cst = ...] which produced something of use.
The asserts come from 359e4ffe3 and before (2006 and before). In those
times [Typeops.infer] rebuilt the term being typed, but nowadays the
assert seems of little use.
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 eeb9c421a..ad13a919d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -256,11 +256,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 @@ -289,7 +286,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 |