diff options
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) = |