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
(Tacticals.thens
~start:(intros_tac ())
~continuations:
- [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None])
+ [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern])
;;
exception NotConvertible
(*CSC: while [what] can have a richer context (because of binders) *)
(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
(*CSC: Is that evident? Is that right? Or should it be changed? *)
-let change_tac ~what ~with_what =
- let change_tac ~what ~with_what (proof, goal) =
+let change_tac ~what ~with_what ~pattern =
+(*
+ let change_tac ~what ~with_what ~pattern (proof, goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* are_convertible works only on well-typed terms *)
else
raise (ProofEngineTypes.Fail "Not convertible")
in
- mk_tactic (change_tac ~what ~with_what)
-
+ mk_tactic (change_tac ~what ~with_what ~pattern)
+*) assert false