C.MutConstruct (uri,tyno,consno,exp_named_subst')
| _ -> [],newmeta,[],term
in
- let metasenv' = newmetasenvfragment@metasenv in
+ let metasenv' = metasenv@newmetasenvfragment in
prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ;
let termty =
CicSubstitution.subst_vars exp_named_subst_diff
let (consthead,newmetas,arguments,_) =
new_metasenv_for_apply newmeta' proof context termty
in
- let newmetasenv = newmetas@metasenv' in
+ let newmetasenv = metasenv'@newmetas in
let subst,newmetasenv' =
CicUnification.fo_unif newmetasenv context consthead ty
in
let elim_simpl_intros_tac ~term =
Tacticals.then_ ~start:(elim_tac ~term)
~continuation:
- (Tacticals.then_ ~start:ReductionTactics.simpl_tac
+ (Tacticals.then_
+ ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
~continuation:(intros_tac ~name:"FOO"))
;;