Removing dead code in Pcoq.

5 files changed, 22 insertions, 46 deletions

diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index ae18925ea..42fc73878 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -11,10 +11,6 @@ Loc
 CList
 CString
 
-Segmenttree
-Unicodetable
-Unicode
-
 Tok
 Compat
 
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 2cf590b1d..8c4930806 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -206,14 +206,14 @@ type notation_grammar = {
 let extend_constr_constr_notation ng =
   let level = ng.notgram_level in
   let mkact loc env = CNotation (loc, ng.notgram_notation, env) in
-  let e = interp_constr_entry_key false (ETConstr (level, ())) in
+  let e = interp_constr_entry_key false level in
   let ext = (ETConstr (level, ()), ng.notgram_assoc) in
   extend_constr e ext (make_constr_action mkact) false ng.notgram_prods
 
 let extend_constr_pat_notation ng =
   let level = ng.notgram_level in
   let mkact loc env = CPatNotation (loc, ng.notgram_notation, env, []) in
-  let e = interp_constr_entry_key true (ETConstr (level, ())) in
+  let e = interp_constr_entry_key true level in
   let ext = ETConstr (level, ()), ng.notgram_assoc in
   extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods
 
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b769a3cbc..bf46fffff 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -77,8 +77,8 @@ type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
 | Aentry : 'a Entry.t -> ('self, 'a) entry_key
 | Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
 
-type 's entry_name = EntryName :
-  'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's entry_name
+type entry_name = EntryName :
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) entry_key -> entry_name
 
 (** Grammar extensions *)
 
@@ -586,7 +586,7 @@ let adjust_level assoc from = function
 	| ETConstr (p,()) -> Some (Some (n, Int.equal n p))
 	| _ -> Some (Some (n,false))
 
-let compute_entry allow_create adjust forpat = function
+let compute_entry adjust forpat = function
   | ETConstr (n,q) ->
       (if forpat then weaken_entry Constr.pattern
        else weaken_entry Constr.operconstr),
@@ -604,26 +604,19 @@ let compute_entry allow_create adjust forpat = function
   | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.")
   | ETOther (u,n) ->
       let u = get_univ u in
-      let e =
-        try get_entry u n
-        with Not_found when allow_create ->
-          let wit = rawwit wit_constr in
-          TypedEntry (wit, create_generic_entry u n wit)
-      in
+      let e = get_entry u n in
       object_of_typed_entry e, None, true
 
 (* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key forpat = function
-  | ETConstr(200,()) when not forpat ->
-      weaken_entry Constr.binder_constr, None
-  | e ->
-      let (e,level,_) = compute_entry true (fun (n,()) -> Some n) forpat e in
-      (e, level)
+let interp_constr_entry_key forpat level =
+  if level = 200 && not forpat then weaken_entry Constr.binder_constr, None
+  else if forpat then weaken_entry Constr.pattern, Some level
+  else weaken_entry Constr.operconstr, Some level
 
 (* This computes the name to give to a production knowing the name and
    associativity of the level where it must be added *)
 let interp_constr_prod_entry_key ass from forpat en =
-  compute_entry false (adjust_level ass from) forpat en
+  compute_entry (adjust_level ass from) forpat en
 
 (**********************************************************************)
 (* Binding constr entry keys to symbols                               *)
@@ -759,17 +752,11 @@ let atactic n =
 
 let try_get_entry u s =
   (** Order the effects: get_entry can raise Not_found *)
-  let TypedEntry (typ, _) = get_entry u s in
-  EntryName (typ, Aentry (Entry.unsafe_of_name (Entry.univ_name u, s)))
-
-type _ target =
-| TgAny : 's target
-| TgTactic : int -> Tacexpr.raw_tactic_expr target
+  let TypedEntry (typ, e) = get_entry u s in
+  EntryName (typ, Aentry (name_of_entry e))
 
 (** Quite ad-hoc *)
-let get_tacentry (type s) (n : int) (t : s target) : s entry_name = match t with
-| TgAny -> EntryName (rawwit wit_tactic, atactic n)
-| TgTactic m ->
+let get_tacentry n m =
   let check_lvl n =
     Int.equal m n
     && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 64f6f720c..e57da42cb 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -153,8 +153,6 @@ type gram_universe = Entry.universe
 
 val get_univ : string -> gram_universe
 
-type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry
-
 val uprim : gram_universe
 val uconstr : gram_universe
 val utactic : gram_universe
@@ -163,8 +161,6 @@ val uvernac : gram_universe
 val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
 val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
 
-val get_entry : gram_universe -> string -> typed_entry
-
 val create_generic_entry : gram_universe -> string ->
   ('a, rlevel) abstract_argument_type -> 'a Gram.entry
 
@@ -267,7 +263,7 @@ val main_entry : (Loc.t * vernac_expr) option Gram.entry
 (** Binding constr entry keys to entries and symbols *)
 
 val interp_constr_entry_key : bool (** true for cases_pattern *) ->
-  constr_entry_key -> grammar_object Gram.entry * int option
+  int -> grammar_object Gram.entry * int option
 
 val symbol_of_constr_prod_entry_key : gram_assoc option ->
   constr_entry_key -> bool -> constr_prod_entry_key ->
@@ -279,16 +275,13 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
 (** Binding general entry keys to symbols *)
 
-type 's entry_name = EntryName :
-  'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's entry_name
-
-(** Interpret entry names of the form "ne_constr_list" as entry keys   *)
-
-type _ target = TgAny : 's target | TgTactic : int -> raw_tactic_expr target
-
-val interp_entry_name : 's target -> string -> string -> 's entry_name
+type entry_name = EntryName :
+  'a raw_abstract_argument_type * (raw_tactic_expr, 'a) entry_key -> entry_name
 
-val parse_user_entry : string -> string -> user_symbol
+(** [interp_entry_name lev n sep] returns the entry corresponding to the name
+    [n] of the form "ne_constr_list" in a tactic entry of level [lev] with
+    separator [sep]. *)
+val interp_entry_name : int -> string -> string -> entry_name
 
 (** Recover the list of all known tactic notation entries. *)
 val list_entry_names : unit -> (string * argument_type) list
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 82bd5dac4..e5edc7422 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -48,7 +48,7 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 let interp_prod_item lev = function
   | TacTerm s -> GramTerminal s
   | TacNonTerm (loc, nt, (_, sep)) ->
-      let EntryName (etyp, e) = interp_entry_name (TgTactic lev) nt sep in
+      let EntryName (etyp, e) = interp_entry_name lev nt sep in
       GramNonTerminal (loc, etyp, e)
 
 let make_terminal_status = function