type 'a eval_from_moo =
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-let coercion_moo_statement_of (uri,arity, saturations) =
+let coercion_moo_statement_of (uri,arity, saturations,_) =
GrafiteAst.Coercion
(HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
saturations (GrafiteTypes.get_baseuri status)
in
let moo_content =
- List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
+ List.map coercion_moo_statement_of ((uri,arity,saturations,0)::compounds)
in
let status = GrafiteTypes.add_moo_content moo_content status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
- List.map (fun u,_,_ -> u) compounds
+ List.map (fun u,_,_,_ -> u) compounds
module MatitaStatus =
struct
in
let is_a_coercion, arity_coercion = is_a_coercion uri in
if is_a_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_coercion,0))
+ Some (uri, coercion_moo_statement_of (uri,arity_coercion,0,0))
else if is_a_wanted_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_wanted,0))
+ Some (uri, coercion_moo_statement_of (uri,arity_wanted,0,0))
else
None)
lemmas)
} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command
~disambiguate_macro opts status (text,prefix_len,ex) ->
match ex with
- | GrafiteAst.Tactic (_, Some tac, punct) ->
+ | GrafiteAst.Tactic (loc, Some tac, punct) ->
let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
let status = eval_tactical status (tactic_of_ast' tac) in
+ (* CALL auto on every goal, easy way of testing it *)
+ let auto =
+ GrafiteAst.AutoBatch
+ (loc, ([],["depth","1";"timeout","1";"type","1"])) in
+ (try
+ let auto = apply_tactic ~disambiguate_tactic ("",0,auto) in
+ let _ = eval_tactical status (tactic_of_ast' auto) in ()
+ with _ -> ());
eval_tactical status
(punctuation_tactical_of_ast (text,prefix_len,punct)),[]
| GrafiteAst.Tactic (_, None, punct) ->