in
let metasenv' = metasenv@newmetasenvfragment in
let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
let termty =
CicSubstitution.subst_vars exp_named_subst_diff termty
in
-(* prerr_endline ("term:" ^ CicPp.ppterm term);*)
-(* prerr_endline ("termty:" ^ CicPp.ppterm termty);*)
let subst,newmetasenv',t =
try
new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty
in
mk_tactic (intros_tac ~mk_fresh_name_callback ())
-let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
let cut_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
term (proof, goal)
in
mk_tactic (cut_tac ~mk_fresh_name_callback term)
-let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
let letin_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
term (proof, goal)
(Tacticals.thens
~start:(intros_tac ())
~continuations:
- [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None])
+ [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern])
;;
exception NotConvertible