1 files changed, 0 insertions, 89 deletions
diff --git a/src/smtlib2/smtlib2_lex.mll b/src/smtlib2/smtlib2_lex.mll
deleted file mode 100644
index 2b965af..0000000
--- a/src/smtlib2/smtlib2_lex.mll
+++ /dev/null
@@ -1,89 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq, originally belong to The Alt-ergo theorem prover           *)
-(*     Copyright (C) 2006-2010                                            *)
-(*                                                                        *)
-(*     Sylvain Conchon                                                    *)
-(*     Evelyne Contejean                                                  *)
-(*     Stephane Lescuyer                                                  *)
-(*     Mohamed Iguernelala                                                *)
-(*     Alain Mebsout                                                      *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-{
-open Lexing
-open Smtlib2_parse
-
-
-let newline lexbuf =
-    let pos = lexbuf.lex_curr_p in
-    lexbuf.lex_curr_p <-
-      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum;
-        pos_cnum=0 }
-
-}
-
-rule token = parse
-| ['\t' ' ' ]+
-    { token lexbuf }
-| ';'  (_ # '\n')*
-     { token lexbuf }
-| ['\n']+ as str
-     { newline lexbuf;
-       Smtlib2_util.line := (!Smtlib2_util.line + (String.length str));
-       token lexbuf }
-| "_"              { UNDERSCORE }
-| "("              { LPAREN }
-| ")"              { RPAREN }
-| "as"             { AS }
-| "let"            { LET }
-| "forall"         { FORALL }
-| "exists"         { EXISTS }
-| "!"              { EXCLIMATIONPT }
-| "set-logic"      { SETLOGIC }
-| "set-option"     { SETOPTION }
-| "set-info"       { SETINFO }
-| "declare-sort"   { DECLARESORT }
-| "define-sort"    { DEFINESORT }
-| "declare-fun"    { DECLAREFUN }
-| "define-fun"     { DEFINEFUN }
-| "push"           { PUSH }
-| "pop"            { POP }
-| "assert"         { ASSERT }
-| "check-sat"      { CHECKSAT }
-| "get-assertions" { GETASSERT }
-| "get-proof"      { GETPROOF }
-| "get-unsat-core" { GETUNSATCORE }
-| "get-value"      { GETVALUE }
-| "get-assignment" { GETASSIGN }
-| "get-option"     { GETOPTION }
-| "get-info"       { GETINFO }
-| "exit"           { EXIT }
-|  '#' 'x' ['0'-'9' 'A'-'F' 'a'-'f']+  as str
-    { HEXADECIMAL(str) }
-|  '#' 'b' ['0'-'1']+  as str
-    { BINARY(str) }
-|  '|' ([ '!'-'~' ' ' '\n' '\t' '\r'] # ['\\' '|'])* '|'  as str
-    { ASCIIWOR(str) }
-|  ':' ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=' '%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']+  as str
-    { KEYWORD(str) }
-|  ['a'-'z' 'A'-'Z' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@'] ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']*  as str
-    { SYMBOL(str) }
-|  '"' (([ '!'-'~' ' ' '\n' '\t' '\r' ] # ['\\' '"']) | ('\\' ['!'-'~' ' ' '\n' '\t' '\r'] ))* '"' as str
-    { STRINGLIT(str) }
-|  ( '0' | ['1'-'9'] ['0'-'9']* )  as str
-    { NUMERAL(str) }
-|  ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str
-    { DECIMAL(str) }
-| eof
-    { EOF }
-| _
-    {failwith(
-      (Lexing.lexeme lexbuf) ^
-	": lexing error on line "^(string_of_int !Smtlib2_util.line))}{}