diff options
| author | Hugo Herbelin | 2016-06-01 20:52:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-02 14:16:11 +0200 |
| commit | 39741ee5b9c5ea1948e2a97e00e362eea6d936d0 (patch) | |
| tree | a53a512eb36f066804382c4d7943f2daf770f910 /intf/notation_term.mli | |
| parent | 5cb0d0590eb01e0122c37904dbfdd53f0405d7f4 (diff) | |
Removing pointless field NPatVar. It does not make sense to have Meta
and Evar in notations, and there are anyway already forbidden.
Diffstat (limited to 'intf/notation_term.mli')
| -rw-r--r-- | intf/notation_term.mli | 1 |
1 files changed, 0 insertions, 1 deletions
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; |