From ba63f39be8e26e04e94d1db7fcc534ad5f732871 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 11 Sep 2018 10:23:02 +0200
Subject: Revert #6651: Use r.(p) syntax to print primitive projections

Fixes #6764: Printing Notation regressed compared to 8.7
---
 interp/notation_term.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp/notation_term.ml')

diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 942ea5ff3f..5fb0ca1b43 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -43,7 +43,6 @@ type notation_constr =
       notation_constr array * notation_constr array
   | NSort of glob_sort
   | NCast of notation_constr * notation_constr cast_type
-  | NProj of Projection.t * notation_constr
 
 (** Note concerning NList: first constr is iterator, second is terminator;
     first id is where each argument of the list has to be substituted
-- 
cgit v1.2.3