| GrafiteAst.Split _ -> Tactics.split
| GrafiteAst.Symmetry _ -> Tactics.symmetry
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
+ (* Implementazioni Aggiunte *)
+ | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
+ | GrafiteAst.Suppose (_, t, id) -> Declarative.suppose t id
+ | GrafiteAst.By_term_we_proved (_, t, ty, id) ->
+ Declarative.by_term_we_proved t ty id
+ | GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove t id
+ | GrafiteAst.Bydone (_, t) -> Declarative.bydone t
(* maybe we only need special cases for apply and goal *)
let classify_tactic tactic =
let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
let status,uris =
match cmd with
+ | GrafiteAst.Print (_,"proofterm") ->
+ let _,_,p,_ = GrafiteTypes.get_current_proof status in
+ print_endline (AutoTactic.pp_proofterm p);
+ status,[]
+ | GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status,[]
LibraryClean.clean_baseuris [value];
assert (Http_getter_storage.is_empty value);
end;
- HExtlib.mkdir
- (Filename.dirname (Http_getter.filename ~writable:true (value ^
- "/foo.con")));
+ if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
+ ~default:false)
+ then
+ HExtlib.mkdir
+ (Filename.dirname (Http_getter.filename ~writable:true (value ^
+ "/foo.con")));
end;
GrafiteTypes.set_option status name value,[]
| GrafiteAst.Drop loc -> raise Drop