diff options
| author | Gaëtan Gilbert | 2018-06-23 15:38:00 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 13:49:17 +0200 |
| commit | 0108db19c96e1b46346f032964f2cca3f8149cb3 (patch) | |
| tree | 6414910c08328fceeb45c82414bea1ee0b601c91 /kernel/mod_subst.ml | |
| parent | 7817af48a554573fb649028263ecfc0fabe400d8 (diff) | |
Projections use index representation
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
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') |