diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 6 |
2 files changed, 3 insertions, 5 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 4f2935be51..13e1abacc1 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -471,7 +471,7 @@ let compare_head_gen eq_universes eq_sorts f t1 t2 = | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 - | Sort s1, Sort s2 -> Sorts.equal s1 s2 + | Sort s1, Sort s2 -> eq_sorts s1 s2 | Cast (c1,_,_), _ -> f c1 t2 | _, Cast (c2,_,_) -> f t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2 diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 0959fa7033..8c4ec8cbfc 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -146,7 +146,7 @@ let infer_declaration env kn dcl = let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let env = push_context_set ctx env in + assert(Univ.ContextSet.is_empty ctx); let body = handle_side_effects env body side_eff in let def, typ, proj = match c.const_entry_proj with @@ -172,9 +172,7 @@ let infer_declaration env kn dcl = let def = Def (Mod_subst.from_val j.uj_val) in def, typ, None in - let univs = Univ.UContext.union c.const_entry_universes - (Univ.ContextSet.to_context ctx) - in + let univs = c.const_entry_universes in feedback_completion_typecheck feedback_id; def, typ, proj, c.const_entry_polymorphic, univs, c.const_entry_inline_code, c.const_entry_secctx |