exception Fail of string Lazy.t
(**
- calls the opaque tactic on the status, restoring the original
- universe graph if the tactic Fails
+ calls the opaque tactic on the status
*)
let apply_tactic t status =
- t status
+ let (uri,metasenv,bo,ty), gl = t status in
+ match
+ CicRefine.pack_coercion_obj
+ (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],[]))
+ with
+ | Cic.CurrentProof (_,metasenv,_,ty,_,_) ->
+ (uri,metasenv,bo,ty), gl
+ | _ -> assert false
+;;
(** constraint: the returned value will always be constructed by Cic.Name **)
type mk_fresh_name_type =