Removing dynamic entries from Pcoq.

5 files changed, 8 insertions, 25 deletions

diff --git a/parsing/entry.ml b/parsing/entry.ml
index 97d601320d..0519903d3d 100644
--- a/parsing/entry.ml
+++ b/parsing/entry.ml
@@ -11,9 +11,7 @@ open Util
 
 type 'a t = string * string
 
-type repr =
-| Static of string * string
-| Dynamic of string
+type repr = string * string
 
 type universe = string
 
@@ -58,6 +56,4 @@ let unsafe_of_name (u, s) =
   assert (String.Set.mem uname !entries);
   (u, s)
 
-let repr = function
-| ("", u) -> Dynamic u
-| (u, s) -> Static (u, s)
+let repr (u, s) = (u, s)
diff --git a/parsing/entry.mli b/parsing/entry.mli
index 6854a5cb45..97cd5b1105 100644
--- a/parsing/entry.mli
+++ b/parsing/entry.mli
@@ -14,9 +14,7 @@ type 'a t
     unique names made of a universe and an entry name. They should be kept
     synchronized with the {!Pcoq} entries though. *)
 
-type repr =
-| Static of string * string
-| Dynamic of string
+type repr = string * string
 (** Representation of entries. *)
 
 (** Table of Coq statically defined grammar entries *)
@@ -41,10 +39,6 @@ val create : universe -> string -> 'a t
 
 (** {5 Meta-programming} *)
 
-val dynamic : string -> 'a t
-(** Dynamic entries. They refer to entries defined in the code source and may
-    only be used in meta-programming definitions from the grammar directory. *)
-
 val repr : 'a t -> repr
 
 val unsafe_of_name : (string * string) -> 'a t
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index c8cd16aaf4..291e919d85 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -224,10 +224,7 @@ let get_entry u s =
   Hashtbl.find utab s
 
 let get_typed_entry e =
-  let (u, s) = match Entry.repr e with
-  | Entry.Dynamic _ -> assert false
-  | Entry.Static (u, s) -> (u, s)
-  in
+  let (u, s) = Entry.repr e in
   let u = Entry.get_univ u in
   get_entry u s
 
@@ -822,7 +819,7 @@ let rec parse_user_entry s sep =
     let s = match s with "hyp" -> "var" | _ -> s in
     Uentry s
 
-let rec interp_entry_name static up_level s sep =
+let rec interp_entry_name up_level s sep =
   let rec eval = function
   | Ulist1 e ->
     let EntryName (t, g) = eval e in
@@ -847,10 +844,7 @@ let rec interp_entry_name static up_level s sep =
       try try_get_entry uprim s with Not_found ->
       try try_get_entry uconstr s with Not_found ->
       try try_get_entry utactic s with Not_found ->
-	if static then
-	  error ("Unknown entry "^s^".")
-	else
-	  EntryName (unsafe_of_genarg (ExtraArgType s), Aentry (Entry.dynamic s))
+      error ("Unknown entry "^s^".")
     end
   | Uentryl (s, n) ->
     (** FIXME: do better someday *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index aa2e092adc..816220b47d 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -283,8 +283,7 @@ type 's entry_name = EntryName :
 
 type _ target = TgAny : 's target | TgTactic : int -> raw_tactic_expr target
 
-val interp_entry_name : bool (** true to fail on unknown entry *) ->
-  's target -> string -> string -> 's entry_name
+val interp_entry_name : 's target -> string -> string -> 's entry_name
 
 val parse_user_entry : string -> string -> user_symbol
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6919729fe9..9a27ae7df4 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 true (TgTactic lev) nt sep in
+      let EntryName (etyp, e) = interp_entry_name (TgTactic lev) nt sep in
       GramNonTerminal (loc, etyp, e)
 
 let make_terminal_status = function