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 /interp/notation_ops.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 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ab0bf9c6fe..7cde563cd2 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -641,11 +641,9 @@ let rec subst_notation_constr subst bound raw = if r1' == r1 && k' == k then raw else NCast(r1',k') | NProj (p, c) -> - let kn = Projection.constant p in - let b = Projection.unfolded p in - let kn' = subst_constant subst kn in + let p' = subst_proj subst p in let c' = subst_notation_constr subst bound c in - if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c') + if p' == p && c' == c then raw else NProj(p', c') let subst_interpretation subst (metas,pat) = |