aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_constr.mlg
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_constr.mlg')
-rw-r--r--parsing/g_constr.mlg10
1 files changed, 0 insertions, 10 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 963f029766..c19dd00b38 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -26,16 +26,6 @@ open Pcoq.Constr
(* TODO: avoid this redefinition without an extra dep to Notation_ops *)
let ldots_var = Id.of_string ".."
-let constr_kw =
- [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
- "end"; "as"; "let"; "if"; "then"; "else"; "return";
- "SProp"; "Prop"; "Set"; "Type";
- ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>";
- ".("; "()"; "`{"; "`("; "@{"; "{|";
- "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ]
-
-let _ = List.iter CLexer.add_keyword constr_kw
-
let mk_cast = function
(c,(_,None)) -> c
| (c,(_,Some ty)) ->