*)
let rewrite_tac ~term:equality =
- let rewrite_tac ~term:equality (proof,goal) =
- let module C = Cic in
- let module U = UriManager in
- let curi,metasenv,pbo,pty = proof in
- let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+ let rewrite_tac ~term:equality (proof,goal) =
+ let module C = Cic in
+ let module U = UriManager in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+ let ty_eq,_ =
+ CicTypeChecker.type_of_aux' metasenv context equality
+ CicUniv.empty_ugraph in
let eq_ind_r,ty,t1,t2 =
- match CicTypeChecker.type_of_aux' metasenv context equality with
+ match ty_eq with
C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
let eq_ind_r =
[eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])) ((curi,metasenv',pbo,pty),goal)
in
assert (List.length goals = 0) ;
- (proof',[fresh_meta])
- in
- ProofEngineTypes.mk_tactic (rewrite_tac ~term:equality)
+ (proof',[fresh_meta])
+ in
+ ProofEngineTypes.mk_tactic (rewrite_tac ~term:equality)
;;
(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
status
in
- ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
+ ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
;;
let module U = UriManager in
let curi,metasenv,pbo,pty = proof in
let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+ let ty_eq,_ =
+ CicTypeChecker.type_of_aux' metasenv context equality
+ CicUniv.empty_ugraph in
let eq_ind_r,ty,t1,t2 =
- match CicTypeChecker.type_of_aux' metasenv context equality with
+ match ty_eq with
C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
let eq_ind_r =
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
- let _,metasenv,_,_ = proof in
- let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let wty = CicTypeChecker.type_of_aux' metasenv context what in
- try
- if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
- then
+ let _,metasenv,_,_ = proof in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
+ let wty,u = (* TASSI: FIXME *)
+ CicTypeChecker.type_of_aux' metasenv context what CicUniv.empty_ugraph in
+ let wwty,_ = CicTypeChecker.type_of_aux' metasenv context with_what u in
+ try
+ if (wty = wwty) then
ProofEngineTypes.apply_tactic
- (T.thens
- ~start:(
- P.cut_tac
- (C.Appl [
- (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ;
- wty ;
- what ;
- with_what]))
- ~continuations:[
- T.then_
- ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
- ~continuation:(
- ProofEngineStructuralRules.clear
- ~hyp:(List.hd context)) ;
- T.id_tac])
+ (T.thens
+ ~start:(
+ P.cut_tac
+ (C.Appl [
+ (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ;
+ wty ;
+ what ;
+ with_what]))
+ ~continuations:[
+
+ T.then_ ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
+ ~continuation:(
+ ProofEngineStructuralRules.clear
+ ~hyp:(List.hd context)) ;
+ T.id_tac])
status
- else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
- with (Failure "hd") ->
- raise (ProofEngineTypes.Fail "Replace: empty context")
+ else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
+ with (Failure "hd") ->
+ raise (ProofEngineTypes.Fail "Replace: empty context")
in
- ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
+ ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
;;