diff --git a/bin/main.ml b/bin/main.ml index 44640ddeab306f5d1dbbf8d93cc569dbd9e3a3ac..37a84ff6579e16ac47db7857a965b006e3fafa8b 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -34,7 +34,7 @@ let gen (args : string array) = else let list_args = Array.to_list args in let name = args.(1) in - let (proof_name, type_name, overwrite,repo_gen, graph_gen) = parse_args list_args ((Filename.basename name)^"_proof") ((Filename.basename name)^"_world_type") true "./generate" false in + let (proof_name, type_name, overwrite,repo_gen, graph_gen) = parse_args list_args ((Filename.basename name)^"_proof") ((Filename.basename name)^"_world_type") true "." false in Gencoq.generate_coq_2files (Interface.parse_description name) (Filename.basename name) proof_name type_name overwrite repo_gen graph_gen ;; diff --git a/lib/lexer.mll b/lib/lexer.mll index be04b7a5e38b59ac293851759505765ae63a5b30..cd243a934db704ddda969d337df7cbf7fceecb73 100644 --- a/lib/lexer.mll +++ b/lib/lexer.mll @@ -10,7 +10,7 @@ let float = integer '.' integer let alpha = ['a'-'z' 'A'-'Z'] let space = [' ' '\t']+ let variable = (alpha | integer | '_')+ -let keyword = ['A'-'Z']alpha+ +let keyword = ['A'-'Z']alpha* rule token = parse | "World" {WORLD} | "Robogram" {ROBOGRAM}