diff options
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index c7a84f6170..c06358054e 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -126,16 +126,13 @@ let expmod_constr cache modlist c = | Not_found -> Constr.map substrec c) | Proj (p, c') -> - (try - (** No need to expand parameters or universes for projections *) - let map cst = - let _ = Cmap.find cst (fst modlist) in - pop_con cst - in - let p = Projection.map map p in - let c' = substrec c' in - mkProj (p, c') - with Not_found -> Constr.map substrec c) + let map cst npars = + let _, newpars = Mindmap.find cst (snd modlist) in + pop_mind cst, npars + Array.length newpars + in + let p' = try Projection.map_npars map p with Not_found -> p in + let c'' = substrec c' in + if p == p' && c' == c'' then c else mkProj (p', c'') | _ -> Constr.map substrec c @@ -157,7 +154,7 @@ type result = { cook_type : types; cook_universes : constant_universes; cook_inline : inline; - cook_context : Context.Named.t option; + cook_context : Constr.named_context option; } let on_body ml hy f = function @@ -204,7 +201,7 @@ let lift_univs cb subst auctx0 = let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in subst, (Polymorphic_const (AUContext.union auctx0 auctx')) -let cook_constant ~hcons env { from = cb; info } = +let cook_constant ~hcons { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in |