match get_proof () with
None -> assert false
| Some (uri, metasenv, bo, ty) ->
+ let uri = match uri with Some uri -> uri | None -> assert false in
let currentproof =
(*CSC: Wrong: [] is just plainly wrong *)
- Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+ Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])
in
let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
- Cic2acic.acic_object_of_cic_object currentproof
+ Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
in
let xml, bodyxml =
match
;;
let apply_tactic ~tactic =
+ let module PET = ProofEngineTypes in
match get_proof (),!goal with
| None,_
| _,None -> assert false
| Some proof', Some goal' ->
- let (newproof, newgoals) = tactic ~status:(proof', goal') in
+ let (newproof, newgoals) = PET.apply_tactic tactic (proof', goal') in
set_proof (Some newproof);
goal :=
(match newgoals, newproof with
let intros ?mk_fresh_name_callback () =
apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ())
let cut ?mk_fresh_name_callback term =
- apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback term)
+ apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback ~term)
let letin ?mk_fresh_name_callback term =
- apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback term)
+ apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback ~term)
let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
let elim_intros_simpl term =
apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
+(* let auto ~dbd () = apply_tactic (AutoTactic.auto_tac ~dbd) *)
+let auto ~dbd () = apply_tactic (AutoTactic.auto_tac_new ~dbd)
+
+
let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)
let replace ~goal_input:what ~input:with_what =