diff options
| author | Pierre-Marie Pédrot | 2016-01-17 00:36:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-17 00:39:06 +0100 |
| commit | 43490147b0749f46eb90ff69c3bbdb3991fb526c (patch) | |
| tree | c76feba268ae1dd33a3ac8e1d931d94fe6a72b78 /parsing/entry.mli | |
| parent | e6b05180d789fb46bc91c71bc97efaf8b552f0fd (diff) | |
Removing dynamic entries from Pcoq.
Diffstat (limited to 'parsing/entry.mli')
| -rw-r--r-- | parsing/entry.mli | 8 |
1 files changed, 1 insertions, 7 deletions
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 |