From 839e87fffdf2634b841aeba6de6d36a2d7a27dbd Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 13 Jun 2017 22:16:46 +0200 Subject: 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. --- kernel/term_typing.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'kernel/term_typing.ml') 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 -- cgit v1.2.3