aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--checker/cic.mli2
-rw-r--r--checker/declarations.ml9
-rw-r--r--checker/values.ml4
3 files changed, 10 insertions, 5 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index 27e2a479f..7ec345768 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -128,7 +128,7 @@ type section_context = unit
(** {6 Substitutions} *)
type delta_hint =
- | Inline of int * constr option
+ | Inline of int * (Univ.AUContext.t * constr) option
| Equiv of KerName.t
type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
diff --git a/checker/declarations.ml b/checker/declarations.ml
index e1d2cf6d1..a744a0227 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -196,7 +196,12 @@ let subst_con0 sub con u =
let dup con = con, Const (con, u) in
let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
match constant_of_delta_with_inline resolve con' with
- | Some t -> con', t
+ | Some (ctx, t) ->
+ (** FIXME: we never typecheck the inlined term, so that it could well
+ be garbage. What environment do we type it in though? The substitution
+ code should be moot in the checker but it **is** used nonetheless. *)
+ let () = assert (Univ.AUContext.size ctx == Univ.Instance.length u) in
+ con', subst_instance_constr u t
| None ->
let con'' = match side with
| User -> constant_of_delta resolve con'
@@ -340,7 +345,7 @@ let gen_subst_delta_resolver dom subst resolver =
let kkey' = if dom then subst_kn subst kkey else kkey in
let hint' = match hint with
| Equiv kequ -> Equiv (subst_kn_delta subst kequ)
- | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+ | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
| Inline (_,None) -> hint
in
Deltamap.add_kn kkey' hint' rslv
diff --git a/checker/values.ml b/checker/values.ml
index f7ab95fe2..67032bd1b 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli
+MD5 fb80632357e3ffa988c6bba3fa6ade64 checker/cic.mli
*)
@@ -173,7 +173,7 @@ let v_section_ctxt = v_enum "emptylist" 1
(** kernel/mod_subst *)
let v_delta_hint =
- v_sum "delta_hint" 0 [|[|Int; Opt v_constr|];[|v_kn|]|]
+ v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|]
let v_resolver =
v_tuple "delta_resolver"