new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
;;
-let apply_tac ~term (proof, goal) =
+let apply_tac_verbose ~term (proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
Cic.Appl (term'::arguments)
)
in
- let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
- let (newproof, newmetasenv''') =
- let subst_in =
- CicMetaSubst.apply_subst ((metano,(context, bo'))::subst)
- in
- subst_meta_and_metasenv_in_proof
- proof metano subst_in newmetasenv''
- in
- (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
+ let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
+ let subst_in =
+ (* if we just apply the subtitution, the type is irrelevant:
+ we may use Implicit, since it will be dropped *)
+ CicMetaSubst.apply_subst
+ ((metano,(context, bo', Cic.Implicit None))::subst)
+ in
+ let (newproof, newmetasenv''') =
+ subst_meta_and_metasenv_in_proof
+ proof metano subst_in newmetasenv''
+ in
+ (subst_in,(newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+
+let apply_tac ~term status = snd (apply_tac_verbose ~term status)
+
+let apply_tac_verbose ~term status =
+ try
+ apply_tac_verbose ~term status
+ (* TODO cacciare anche altre eccezioni? *)
+ with CicUnification.UnificationFailure _ as e ->
+ raise (Fail (Printexc.to_string e))
(* TODO per implementare i tatticali e' necessario che tutte le tattiche
sollevino _solamente_ Fail *)