From c5ecebf6fefbaa673dda506175a2aa4a69d79807 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Sep 2014 00:03:46 +0200
Subject: Revert specific syntax for primitive projections, avoiding ugly
 contortions in internalization/externalization. It uses a fully typed version
 of detyping, requiring the environment, to move from primitive projection
 applications to regular applications of the eta-expanded version. The kernel
 is unchanged, and only constrMatching needs compatibility code now.

---
 intf/notation_term.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf/notation_term.mli')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 8bb43e96a5..daf605ab28 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -25,7 +25,6 @@ type notation_constr =
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t * Genarg.glob_generic_argument option
-  | NProj of projection * notation_constr
   | NList of Id.t * Id.t * notation_constr * notation_constr * bool
   (** Part only in [glob_constr] *)
   | NLambda of Name.t * notation_constr * notation_constr
-- 
cgit v1.2.3