aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorcoq2001-05-29 16:59:13 +0000
committercoq2001-05-29 16:59:13 +0000
commit23eeec04be50b3d851f148c2500f94ab9df0574f (patch)
tree4992458ddb33aaac45f81a4ca91fe0085a92db0c /parsing
parent982812b7e66746d588fc9dcf37da21f891cf8948 (diff)
Retablissement de minicoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1773 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_minicoq.ml413
1 files changed, 6 insertions, 7 deletions
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index 6611eba55b..901e686315 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -17,13 +17,12 @@ open Univ
open Term
open Environ
-let lexer = {
- Token.func = Lexer.func;
- Token.using = (function ("",s) -> Lexer.add_keyword s | _ -> ());
- Token.removing = (fun _ -> ());
- Token.tparse = Lexer.tparse;
- Token.text = Lexer.token_text }
-
+let lexer =
+ {Token.func = Lexer.func; Token.using = Lexer.add_token;
+ Token.removing = (fun _ -> ()); Token.tparse = Lexer.tparse;
+ Token.text = Lexer.token_text}
+;;
+
type command =
| Definition of identifier * constr option * constr
| Parameter of identifier * constr