@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
in
aux (n-1) tl
(status_of_single_goal_tactic_result
- (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) 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') ;
ProofEngineTypes.apply_tactic
(Tacticals.first
~tactics:[
- "reflexivity", EqualityTactics.reflexivity_tac ;
- "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
- "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
- "exact sym_eqt su t1 ...", exact_tac
+ EqualityTactics.reflexivity_tac ;
+ exact_tac ~term:t1'_eq_t1'' ;
+ exact_tac ~term:t2'_eq_t2'' ;
+ exact_tac
~term:(
Cic.Appl
[mkConst HelmLibraryObjects.Logic.sym_eq_URI
] ;
t1'_eq_t1''
]) ;
- "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
+ ProofEngineTypes.mk_tactic (fun status ->
let status' = (* status after 1st elim_type use *)
let context = context_of_status status in
let b,_ = (*TASSI : FIXME*)
- are_convertible context t1'' t1 CicUniv.empty_ugraph in
+ are_convertible context t1'' t1 CicUniv.oblivion_ugraph in
if not b then begin
warn (lazy "t1'' and t1 are NOT CONVERTIBLE");
let newstatus =
ProofEngineTypes.apply_tactic
(Tacticals.first (* try to solve 1st subgoal *)
~tactics:[
- "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
- "exact sym_eqt su t2 ...",
- exact_tac
+ exact_tac ~term:t2'_eq_t2'';
+ exact_tac
~term:(
Cic.Appl
[mkConst HelmLibraryObjects.Logic.sym_eq_URI
] ;
t2'_eq_t2''
]) ;
- "elim_type eqt su t2 ...",
ProofEngineTypes.mk_tactic (fun status ->
let status' =
let context = context_of_status status in
let b,_ = (* TASSI:FIXME *)
- are_convertible context t2'' t2 CicUniv.empty_ugraph
+ are_convertible context t2'' t2
+ CicUniv.oblivion_ugraph
in
if not b then begin
warn (lazy "t2'' and t2 are NOT CONVERTIBLE");