Commit de5ec0a4 authored by Heiko Becker's avatar Heiko Becker

Start implementing binary certificate generation

parent 2d2ea6b1
......@@ -87,6 +87,8 @@ case fuel of
| "Ret" => DRET :: lex input'' fuel'
| "Let" => DLET :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| "PRE" => DPRE :: lex input'' fuel'
| "ABS" => DABS :: lex input'' fuel'
| _ => NIL
else
(case char of
......
......@@ -19,7 +19,9 @@ object Main {
val optionPrintToughSMTCalls = FlagOptionDef("print-tough-smt-calls",
"If enabled, will print those SMT queries to file which take longer.")
val optionValidators = ChoiceOptionDef("certificate", "Wether to certify and which theorem prover to use",Set("coq","hol-light","hol4"),"coq")
val optionValidators = ChoiceOptionDef("certificate",
"Wether to certify and which theorem prover to use",
Set("coq", "hol4", "binary"), "coq")
val globalOptions: Set[CmdLineOptionDef[Any]] = Set(
FlagOptionDef("help", "Show this message."),
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment