in
let discriminate'_tac ~term status =
let (proof, goal) = status in
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
(EqualityTactics.rewrite_simpl_tac
~direction:`RightToLeft
~pattern:(ProofEngineTypes.conclusion_pattern None)
- term)
+ term [])
~continuation:
(IntroductionTactics.constructor_tac ~n:1)))) status
| _ -> fail "not an equality"
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let term = CicSubstitution.lift liftno term in
let termty,_ = (* TASSI: FIXME *)
let module P = PrimitiveTactics in
let module T = Tacticals in
let term = CicSubstitution.lift liftno term in
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ = (* TASSI: FIXME *)
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
~start:(ProofEngineTypes.mk_tactic
(fun status ->
let (proof, goal) = status in
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let _,context,gty =
CicUtil.lookup_meta goal metasenv
in
(EqualityTactics.rewrite_simpl_tac
~direction:`LeftToRight
~pattern:(ProofEngineTypes.conclusion_pattern None)
- term)
+ term [])
~continuation:EqualityTactics.reflexivity_tac)
])
status