From 0108db19c96e1b46346f032964f2cca3f8149cb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:38:00 +0200
Subject: Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
---
 interp/notation_ops.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'interp/notation_ops.ml')

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) =
-- 
cgit v1.2.3