From 25cab58df1171c9419396342e9ecc3094b74eca5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Feb 2020 21:09:53 +0100
Subject: Revert "Granting #9516 and #9518 (support for numerals and strings in
 custom entries)."

This reverts commit 29919b725262dca76708192bde65ce82860747be.

It was pushed by mistake as part of #11530. Sorry about it.
---
 parsing/extend.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'parsing/extend.ml')

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 178f7354f2..848861238a 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -29,7 +29,6 @@ type 'a constr_entry_key_gen =
   | ETIdent
   | ETGlobal
   | ETBigint
-  | ETString
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
@@ -54,7 +53,6 @@ type constr_prod_entry_key =
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
-  | ETProdString          (* Parsed as a string *)
   | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
   | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
-- 
cgit v1.2.3