@param proof a proof
@return the uri of a given proof
*)
-let uri_of_proof ~proof:(uri, _, _, _, _) = uri
+let uri_of_proof ~proof:(uri, _, _, _, _, _) = uri
(**
@param status current proof engine status
@raise Failure if proof is None
@return current goal's metasenv
*)
-let metasenv_of_status ((_,m,_,_, _), _) = m
+let metasenv_of_status ((_,m,_,_,_, _), _) = m
(**
@param status a proof engine status
(ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status))
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, _) = CicUtil.lookup_meta goal metasenv in
let proof',goal' = aux count context status in
assert (goal = goal') ;