summaryrefslogtreecommitdiff
path: root/language/l2_parse.ott
diff options
context:
space:
mode:
authorJon French2017-07-21 16:03:01 +0100
committerJon French2017-07-21 20:56:56 +0100
commitccbb4a5dfd4c3bcea6748b122470351519a27674 (patch)
tree2a2acfb964731878ea4b65f6d57f99fdf7ba16be /language/l2_parse.ott
parent2e1ca2e6b77b285168223263e747396ad01cb993 (diff)
l2.ott, l2_parse.ott: remove unnecessary 'type text = string'
Diffstat (limited to 'language/l2_parse.ott')
-rw-r--r--language/l2_parse.ott6
1 files changed, 2 insertions, 4 deletions
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 28803cb6..49df4908 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -41,8 +41,6 @@ metavar regexp ::=
embed
{{ ocaml
-type text = string
-
type l =
| Unknown
| Int of string * l option
@@ -77,7 +75,7 @@ val subst : forall 'a. list 'a -> list 'a -> bool
}}
metavar x , y , z ::=
- {{ ocaml text }}
+ {{ ocaml string }}
{{ lem string }}
{{ hol string }}
{{ com identifier }}
@@ -86,7 +84,7 @@ metavar x , y , z ::=
metavar ix ::=
{{ lex alphanum }}
- {{ ocaml text }}
+ {{ ocaml string }}
{{ lem string }}
{{ hol string }}
{{ com infix identifier }}