diff options
| author | Pierre-Marie Pédrot | 2018-07-24 17:58:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-24 17:58:01 +0200 |
| commit | 3599d05a5b3664764f19a794dc69c4e28f2e135d (patch) | |
| tree | ee65c9840649332663491ead6073f1323f4a6fb5 /kernel/mod_subst.ml | |
| parent | 388e65b550a6dd12fa4e59b26e03a831ebd842ce (diff) | |
| parent | 277563ab74a0529c330343479a063f808baa6db4 (diff) | |
Merge PR #7908: Projections use index representation
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index a47af56ca5..b35b9dda31 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -332,6 +332,12 @@ let subst_constant sub con = try fst (subst_con0 sub (con,Univ.Instance.empty)) with No_subst -> con +let subst_proj_repr sub p = + Projection.Repr.map (subst_mind sub) p + +let subst_proj sub p = + Projection.map (subst_mind sub) p + (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" @@ -346,11 +352,7 @@ let rec map_kn f f' c = match kind c with | Const kn -> (try snd (f' kn) with No_subst -> c) | Proj (p,t) -> - let p' = - try - Projection.map (fun kn -> fst (f' (kn,Univ.Instance.empty))) p - with No_subst -> p - in + let p' = Projection.map f p in let t' = func t in if p' == p && t' == t then c else mkProj (p', t') |