From 39741ee5b9c5ea1948e2a97e00e362eea6d936d0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Jun 2016 20:52:18 +0200
Subject: Removing pointless field NPatVar. It does not make sense to have Meta
 and Evar in notations, and there are anyway already forbidden.

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

(limited to 'intf')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 39a36310d1..7c5d7657be 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -42,7 +42,6 @@ type notation_constr =
       (Name.t * notation_constr option * notation_constr) list array *
       notation_constr array * notation_constr array
   | NSort of glob_sort
-  | NPatVar of patvar
   | NCast of notation_constr * notation_constr cast_type
 
 (** Note concerning NList: first constr is iterator, second is terminator;
-- 
cgit v1.2.3