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
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