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
---
 pretyping/patternops.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index f7fea22c0f..3c1c470053 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -464,9 +464,6 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
 	 one non-trivial branch. These facts are used in [Constrextern]. *)
       PCase (info, pred, pat_of_raw metas vars c, brs)
 
-  | GProj(p,c) ->
-    PProj(p, pat_of_raw metas vars c)
-
   | GRec (GFix (ln,n), ids, decls, tl, cl) ->
     if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
       err ?loc (Pp.str "\"struct\" annotation is expected.")
-- 
cgit v1.2.3