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.ml | |
| parent | e6b05180d789fb46bc91c71bc97efaf8b552f0fd (diff) | |
Removing dynamic entries from Pcoq.
Diffstat (limited to 'parsing/entry.ml')
| -rw-r--r-- | parsing/entry.ml | 8 |
1 files changed, 2 insertions, 6 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) |