- object
- method evalPhrase s: state_tag =
- let command = CicTextualParser2.parse_command (Stream.of_string s) in
- match command with
- | CommandAst.Theorem (_, _, Some name, ast, None) ->
+ object (self)
+ inherit interpreterState ~console
+
+ method evalTactical = function
+(*
+ | TacticAst.Command _ -> failwith "1"
+ | TacticAst.Tactic _ -> failwith "2"
+ | TacticAst.LocatedTactical _ -> failwith "3"
+ | TacticAst.Fail -> failwith "4"
+ | TacticAst.Do (_, _) -> failwith "5"
+ | TacticAst.IdTac -> failwith "6"
+ | TacticAst.Repeat _ -> failwith "7"
+ | TacticAst.Seq _ -> failwith "8"
+ | TacticAst.Then (_, _) -> failwith "9"
+ | TacticAst.Tries _ -> failwith "10"
+ | TacticAst.Try _ -> failwith "11"
+*)
+ | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
+ | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) ->