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/glob_term.mli     | 1 -
 intf/notation_term.mli | 1 -
 2 files changed, 2 deletions(-)

(limited to 'intf')

diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 237d033662..832ee4e4b0 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -41,7 +41,6 @@ type glob_constr =
   | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
       (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in
 	  [MatchStyle]) *)
-  | GProj of Loc.t * projection * glob_constr
   | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) *
       glob_constr * glob_constr
   | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr
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