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 ~eta_fix:false currentproof
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)