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
C.Rel _ -> []
| C.Meta (n,_) -> [n]
| C.Sort _
- | C.Implicit -> []
+ | C.Implicit _ -> []
| C.Cast (te,ty) -> (aux te) @ (aux ty)
| C.Prod (_,s,t) -> (aux s) @ (aux t)
| C.Lambda (_,s,t) -> (aux s) @ (aux t)
match get_proof () with
None -> assert false
| Some (uri,metasenv,bo,gty as proof') ->
- let newmeta = new_meta proof' in
+ let newmeta = new_meta_of_proof proof' in
(* We push the new meta at the end of the list for pretty-printing *)
(* purposes: in this way metas are ordered. *)
let metasenv' = metasenv@[newmeta,context,ty] in
- let irl = identity_relocation_list_for_metavariable context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
let bo' =
ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo
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)