-let applyS_tac ~dbd ~term (proof, goal) =
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let module C = Cic in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
- let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
- match term with
- C.Var (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Var (uri,exp_named_subst')
- | C.Const (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Const (uri,exp_named_subst')
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutInd (uri,tyno,exp_named_subst')
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutConstruct (uri,tyno,consno,exp_named_subst')
- | _ -> [],newmeta,[],term
- in
- let metasenv' = metasenv@newmetasenvfragment in
- let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
- in
- let termty =
- CicSubstitution.subst_vars exp_named_subst_diff termty in
- let goal_arity = count_prods context ty in
- let res =
- new_metasenv_and_unify_and_t dbd proof goal
- newmeta' metasenv' context term' ty termty goal_arity
- in
- res