diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 33 | ||||
| -rw-r--r-- | kernel/univ.mli | 2 |
2 files changed, 27 insertions, 8 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 7c5b8c7283..27ab90aa59 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -70,20 +70,39 @@ let handle_side_effects env body side_eff = let rec sub c i x = match kind_of_term x with | Const (c', _) when eq_constant c c' -> mkRel i | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in + let rec sub_body c u b i x = match kind_of_term x with + | Const (c',u') when eq_constant c c' -> + let subst = + Array.fold_left2 (fun subst l l' -> Univ.LMap.add l l' subst) + Univ.LMap.empty (Instance.to_array u) (Instance.to_array u') + in + Vars.subst_univs_level_constr subst b + | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in let fix_body (c,cb) t = match cb.const_body with | Undef _ -> assert false | Def b -> let b = Mod_subst.force_constr b in - let b_ty = Typeops.type_of_constant_type env cb.const_type in - let t = sub c 1 (Vars.lift 1 t) in - mkLetIn (cname c, b, b_ty, t) + let poly = cb.const_polymorphic in + if not poly then + let b_ty = Typeops.type_of_constant_type env cb.const_type in + let t = sub c 1 (Vars.lift 1 t) in + mkLetIn (cname c, b, b_ty, t) + else + let univs = Future.force cb.const_universes in + sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t) | OpaqueDef b -> let b = Opaqueproof.force_proof b in - let b_ty = Typeops.type_of_constant_type env cb.const_type in - let t = sub c 1 (Vars.lift 1 t) in - mkApp (mkLambda (cname c, b_ty, t), [|b|]) in - List.fold_right fix_body cbl t + let poly = cb.const_polymorphic in + if not poly then + let b_ty = Typeops.type_of_constant_type env cb.const_type in + let t = sub c 1 (Vars.lift 1 t) in + mkApp (mkLambda (cname c, b_ty, t), [|b|]) + else + let univs = Future.force cb.const_universes in + sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t) + in + List.fold_right fix_body cbl t in (* CAVEAT: we assure a proper order *) Declareops.fold_side_effects handle_sideff body diff --git a/kernel/univ.mli b/kernel/univ.mli index c149bb1acc..ea3ab16a51 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -109,7 +109,7 @@ sig val equal : t -> t -> bool (** Equality function on formal universes *) - (* val hash : t -> int *) + val hash : t -> int (** Hash function *) val make : Level.t -> t |