debug ("tac "^str^" :\n" );
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("tac "^str^" :\n" );
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
- PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
+ (fun status -> pall "n0" status _Rlt_zero_1 ;
+ PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in
- (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
- PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
+ (fun status -> pall "d0" status _Rlt_zero_1 ;
+ PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in
- tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
- ~status _Rlt_zero_pos_plus1;
- PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
+ tacn:=(Tacticals.then_ ~start:(fun status -> pall ("n"^string_of_int i)
+ status _Rlt_zero_pos_plus1;
+ PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 status)
- tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
- ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
- ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
+ tacd:=(Tacticals.then_ ~start:(fun status -> pall "d"
+ status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
+ ~term:_Rlt_zero_pos_plus1 status) ~continuation:!tacd);
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
^ CicPp.ppterm ty ^"\n");
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
^ CicPp.ppterm ty ^"\n");
-let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
+let tac_zero_infeq_false gl (n,d) status=
+let (proof, goal) = status in
debug("stat tac_zero_infeq_false\n");
let r =
let curi,metasenv,pbo,pty = proof in
debug("stat tac_zero_infeq_false\n");
let r =
let curi,metasenv,pbo,pty = proof in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
PrimitiveTactics.apply_tac
(*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
PrimitiveTactics.apply_tac
(*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let proof'',goals =
apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
let proof'',goals =
apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
debug("Inizio TC_USE\n");
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug("Inizio TC_USE\n");
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
let (proof,goals) =
EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
let (proof,goals) =
EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
- ~status:((curi,metasenv',pbo,pty),goal)
+ ((curi,metasenv',pbo,pty),goal)
in
let new_goals = fresh_meta::goals in
debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
in
let new_goals = fresh_meta::goals in
debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let num = ref 0 in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let num = ref 0 in
Tacticals.then_
(*inutile sia questo che quello prima della chiamata*)
~start:PrimitiveTactics.intros_tac
~continuation:(Tacticals.then_
~start:(VariousTactics.elim_type_tac ~term:_False)
~continuation:(assumption_tac))
Tacticals.then_
(*inutile sia questo che quello prima della chiamata*)
~start:PrimitiveTactics.intros_tac
~continuation:(Tacticals.then_
~start:(VariousTactics.elim_type_tac ~term:_False)
~continuation:(assumption_tac))
let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
debug ("inizio t1 strict\n");
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
debug ("inizio t1 strict\n");
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
debug("INIZIO TAC 1 2\n");
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
debug("INIZIO TAC 1 2\n");
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
PrimitiveTactics.change_tac ~what:ty
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
PrimitiveTactics.change_tac ~what:ty
~continuation:(Tacticals.then_
~start:(PrimitiveTactics.apply_tac ~term:
(if sres then _Rnot_lt_lt else _Rnot_le_le))
~continuation:(Tacticals.thens
~start:(
~continuation:(Tacticals.then_
~start:(PrimitiveTactics.apply_tac ~term:
(if sres then _Rnot_lt_lt else _Rnot_le_le))
~continuation:(Tacticals.thens
~start:(
debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
(match r with (p,gl) ->
debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
r)
~continuations:
[PrimitiveTactics.apply_tac ~term:_Rinv_R1
;Tacticals.try_tactics
(match r with (p,gl) ->
debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
r)
~continuations:
[PrimitiveTactics.apply_tac ~term:_Rinv_R1
;Tacticals.try_tactics
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* check if ty is of type *)
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* check if ty is of type *)