in
let discriminate'_tac ~term status =
let (proof, goal) = status in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
in
let injection_tac ~term status =
let (proof, goal) = status in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst, _,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let term = CicSubstitution.lift liftno term in
let termty,_ =
* differiscono (o potrebbero differire?) nell'i-esimo parametro
* del costruttore *)
let term = CicSubstitution.lift liftno term in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
(fun status ->
debug_print (lazy "riempo il cut");
let (proof, goal) = status in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,gty =CicUtil.lookup_meta goal metasenv in
let gty = Unshare.unshare gty in
let new_t1' =