Introducing an intermediary type "constr_prod_entry_key" for grammar productions.

This type describes the grammar non-terminal. It typically contains
ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is
the type for metasyntax.ml and egramcoq.ml to communicate together.

The type constr_prod_entry_key with ETConstr, ETBinder, is now used
only in metasyntax.ml. This allows to get rid of some "assert false"
in uselessly matching over ETConstrList in metasyntax.ml and of some
"assert false" in uselessly matching over ETBinder in egramcoq.ml.

Also exporting less of extend.mli in API.

1 files changed, 9 insertions, 14 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 16124c26c..3c4f408f8 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -229,7 +229,6 @@ type (_, _) entry =
 | TTName : ('self, Name.t Loc.located) entry
 | TTReference : ('self, reference) entry
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
-| TTBinder : ('self, local_binder_expr list) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
 | TTOpenBinderList : ('self, local_binder_expr list) entry
@@ -292,23 +291,20 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as
 | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
 | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
 | TTName -> Aentry Prim.name
-| TTBinder -> Aentry Constr.binder
 | TTOpenBinderList -> Aentry Constr.open_binders
 | TTBigint -> Aentry Prim.bigint
 | TTReference -> Aentry Constr.global
 
 let interp_entry forpat e = match e with
-| ETName -> TTAny TTName
-| ETReference -> TTAny TTReference
-| ETBigint -> TTAny TTBigint
-| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList.")
-| ETBinder false  -> TTAny TTBinder
-| ETConstr p -> TTAny (TTConstr (p, forpat))
-| ETPattern -> assert false (** not used *)
-| ETOther _ -> assert false (** not used *)
-| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
-| ETBinderList ETBinderOpen -> TTAny TTOpenBinderList
-| ETBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
+| ETProdName -> TTAny TTName
+| ETProdReference -> TTAny TTReference
+| ETProdBigint -> TTAny TTBigint
+| ETProdConstr p -> TTAny (TTConstr (p, forpat))
+| ETProdPattern -> assert false (** not used *)
+| ETProdOther _ -> assert false (** not used *)
+| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
+| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
+| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
 
 let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
   | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
@@ -334,7 +330,6 @@ match e with
   | ForConstr -> push_constr subst (constr_expr_of_name v)
   | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
   end
-| TTBinder -> { subst with binders = (v, true) :: subst.binders }
 | TTOpenBinderList -> { subst with binders = (v, true) :: subst.binders }
 | TTClosedBinderList _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
 | TTBigint ->