C.MutConstruct (uri,tyno,consno,exp_named_subst')
| _ -> [],newmeta,[],term
in
C.MutConstruct (uri,tyno,consno,exp_named_subst')
| _ -> [],newmeta,[],term
in
prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ;
let termty =
CicSubstitution.subst_vars exp_named_subst_diff
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 (consthead,newmetas,arguments,_) =
new_metasenv_for_apply newmeta' proof context termty
in
let old_uninstantiatedmetas,new_uninstantiatedmetas =
(* subst_in doesn't need the context. Hence the underscore. *)
let subst_in _ = CicUnification.apply_subst subst in
let old_uninstantiatedmetas,new_uninstantiatedmetas =
(* subst_in doesn't need the context. Hence the underscore. *)
let subst_in _ = CicUnification.apply_subst subst in