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 elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
+let auto mqi_handle () = apply_tactic (VariousTactics.auto_tac mqi_handle)
let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)