diff options
| author | coq | 2001-05-29 16:59:13 +0000 |
|---|---|---|
| committer | coq | 2001-05-29 16:59:13 +0000 |
| commit | 23eeec04be50b3d851f148c2500f94ab9df0574f (patch) | |
| tree | 4992458ddb33aaac45f81a4ca91fe0085a92db0c /parsing | |
| parent | 982812b7e66746d588fc9dcf37da21f891cf8948 (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.ml4 | 13 |
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 |
