let module R = CicReduction in
let module S = CicSubstitution in
let module PT = PrimitiveTactics in
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let rec find n = function
hd::tl ->
let module C = Cic in
let module P = PrimitiveTactics in
let module T = Tacticals in
- let uri,metasenv,pbo,pty = proof in
+ let uri,metasenv,_subst,pbo,pty, attrs = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let subst,metasenv,u,selected_hyps,terms_with_context =
ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
else
u1
) u terms_with_context) ;
- let status = (uri,metasenv',pbo,pty),goal in
+ let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in
let proof,goals =
PET.apply_tactic
(T.thens
T.id_tac])
status
in
- let _,metasenv'',_,_ = proof in
+ let _,metasenv'',_subst,_,_, _ = proof in
(* CSC: the following is just a bad approximation since a meta
can be closed and then re-opened! *)
(proof,