X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=c46973e2cbeffab6cffc4a95224136ffb4603d07;hb=c7eb56246dc1199f098ed6c8c77aa08fea9a62f8;hp=446b2ef4b0ac92f95be24194ee6021fc5cb78f27;hpb=04f0e78400f9848f08f5ef194c02002e2c2c75c7;p=helm.git diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 446b2ef4b..c46973e2c 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -24,6 +24,57 @@ *) +(******************** OTHER USEFUL TACTICS **********************) + +let rewrite_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0) + in + eq_ind_r,ty,t1,t2 + | C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0) + in + eqT_ind_r,ty,t1,t2 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality: + (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true) + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + PrimitiveTactics.exact_tac + (C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ((curi,metasenv',pbo,pty),goal) +;; + +(******************** THE FOURIER TACTIC ***********************) (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients des inéquations et équations sont entiers. En attendant la tactique Field. @@ -428,62 +479,49 @@ Construction de la preuve en cas de succ i.e. on obtient une contradiction. *) -let _R = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;; + +let _eqT = Cic.MutInd(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;; +let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;; +let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;; let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;; let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;; +let _R = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;; +let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;; +let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;; +let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;; +let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;; +let _Rfourier_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;; +let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;; +let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;; +let _Rfourier_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;; +let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;; +let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;; +let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;; +let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;; +let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;; +let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;; let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;; +let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;; +let _Rle = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;; let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;; let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;; let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;; let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;; let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;; +let _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;; let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;; let _Rlt_not_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;; let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;; let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;; -let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;; let _Rminus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;; - +let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;; +let _Rnot_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;; let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;; +let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;; let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;; let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;; -let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;; -let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;; -let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;; -let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;; -let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;; - -let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;; -let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;; -let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;; -let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;; -let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;; - -let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;; - -let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;; -let _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;; -let _Rle = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;; -let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;; - let _sym_eqT = Cic.Const(UriManager.uri_of_string "/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;; - -let _Rfourier_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;; -let _Rfourier_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;; - -let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;; - -let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;; - - -let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;; -let _Rnot_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;; - - - - - - +(*****************************************************************************************************) let is_int x = (x.den)=1 ;; @@ -497,6 +535,7 @@ let rec rational_to_fraction x= (x.num,x.den) let rec int_to_real_aux n = match n with 0 -> _R0 (* o forse R0 + R0 ????? *) + | 1 -> _R1 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ] ;; @@ -521,6 +560,8 @@ let rational_to_real x = (* preuve que 0 m=goal) metasenv in + debug ("th = "^ CicPp.ppterm t ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + in + let tacn=ref + (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + let tacd=ref + (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + + + for i=1 to n-1 do + 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) ~continuation:!tacn); done; + for i=1 to d-1 do + tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); done; + + + +debug("TAC ZERO INF POS\n"); +(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) + ~continuations:[ + !tacn ; + !tacd ] + ~status) +;; @@ -570,7 +640,7 @@ let tac_zero_inf_false gl (n,d) = let tac_zero_infeq_false gl (n,d) = (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) - ~continuation:(tac_zero_inf_pos gl (-n,d))) + ~continuation:(tac_zero_inf_pos (-n,d))) ;; @@ -615,18 +685,29 @@ let my_cut ~term:c ~status:(proof,goal)= let exact = PrimitiveTactics.exact_tac;; -let tac_use h = match h.htype with - "Rlt" -> exact ~term:h.hname - |"Rle" -> exact ~term:h.hname - |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) - ~continuation:(exact ~term:h.hname)) - |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le) - ~continuation:(exact ~term:h.hname)) - |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le) - ~continuation:(exact ~term:h.hname)) - |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le) - ~continuation:(exact ~term:h.hname)) - |_->assert false +let tac_use h ~status:(proof,goal as status) = +debug("Inizio TC_USE\n"); +let curi,metasenv,pbo,pty = proof in +let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); +debug ("ty = "^ CicPp.ppterm ty^"\n"); + +let res = +match h.htype with + "Rlt" -> exact ~term:h.hname ~status + |"Rle" -> exact ~term:h.hname ~status + |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) + ~continuation:(exact ~term:h.hname)) ~status + |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |_->assert false +in +debug("Fine TAC_USE\n"); +res ;; @@ -693,23 +774,21 @@ let rec superlift c n= ;; -(* fix !!!!!!!!!! this may not work *) let equality_replace a b ~status = + let module C = Cic in let proof,goal = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in -prerr_endline (" " ^ CicPp.ppterm b) ; -prerr_endline ("### IN MY_CUT: ") ; -prerr_endline ("@ " ^ CicPp.ppterm ty) ; -List.iter (function Some (n,Cic.Decl t) -> prerr_endline ("# " ^ CicPp.ppterm t)) context ; -prerr_endline ("##- IN MY_CUT ") ; -let res = - let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in -(*CSC: codice ad-hoc per questo caso!!! Non funge in generale *) - PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;_R;b;Cic.Lambda(Cic.Name "pippo",_R,Cic.Appl [_not; Cic.Appl [_Rlt;_R0;Cic.Rel 1]])]) ~status -in -prerr_endline "EUREKA" ; -res + let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in + let (proof,goals) = + rewrite_tac ~term:(C.Meta (fresh_meta,irl)) + ~status:((curi,metasenv',pbo,pty),goal) + in + (proof,fresh_meta::goals) ;; let tcl_fail a ~status:(proof,goal) = @@ -862,44 +941,82 @@ let rec fourier ~status:(s_proof,s_goal)= (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *) debug "inizio a costruire tac1\n"; + Fourier.print_rational(c1); - let tac1=ref ( if h1.hstrict then - (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt) - ~continuations:[tac_use h1;tac_zero_inf_pos goal - (rational_to_fraction c1)]) + let tac1=ref ( fun ~status -> + debug ("Sotto tattica t1 "^(if h1.hstrict then "strict" else "lasc")^"\n"); + if h1.hstrict then + (Tacticals.thens ~start:( + fun ~status -> + debug ("inizio t1 strict\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + + PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) + ~continuations:[tac_use h1; + + tac_zero_inf_pos (rational_to_fraction c1)] ~status + + ) else (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) - ~continuations:[tac_use h1;tac_zero_inf_pos goal - (rational_to_fraction c1)])) + ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status)) + in s:=h1.hstrict; List.iter (fun (h,c) -> (if (!s) then (if h.hstrict then + (debug("tac1 1\n"); tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_lt_lt) + ~term:_Rfourier_lt_lt) ~continuations:[!tac1;tac_use h; - tac_zero_inf_pos goal - (rational_to_fraction c)]) + tac_zero_inf_pos + (rational_to_fraction c)])) else - tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_lt_le) + ( + debug("tac1 2\n"); + Fourier.print_rational(c1); + tac1:=(Tacticals.thens ~start:( + fun ~status -> + debug("INIZIO TAC 1 2\n"); + + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + + PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status + + ) ~continuations:[!tac1;tac_use h; - tac_zero_inf_pos goal - (rational_to_fraction c)]) + + tac_zero_inf_pos (rational_to_fraction c) + + ])) ) else (if h.hstrict then + ( + + debug("tac1 3\n"); tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) ~continuations:[!tac1;tac_use h; - tac_zero_inf_pos goal - (rational_to_fraction c)]) + tac_zero_inf_pos + (rational_to_fraction c)])) else - tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) + ( + debug("tac1 4\n"); + tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) ~continuations:[!tac1;tac_use h; - tac_zero_inf_pos goal - (rational_to_fraction c)]))); + tac_zero_inf_pos + (rational_to_fraction c)])) + + ) + ); s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) @@ -917,8 +1034,6 @@ let rec fourier ~status:(s_proof,s_goal)= ~continuation:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le)) - ~continuation:Ring.id_tac -(*CSC ~continuation:(Tacticals.thens ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc) ~continuations:[tac2;(Tacticals.thens @@ -936,7 +1051,7 @@ let rec fourier ~status:(s_proof,s_goal)= ) ] (* end continuations before comment *) - ) *) + ) ); !tac1] );(*end tac:=*) @@ -953,10 +1068,9 @@ let rec fourier ~status:(s_proof,s_goal)= |_-> assert false)(*match (!lutil) *) |_-> assert false); (*match res*) - debug ("finalmente applico t1\n"); + debug ("finalmente applico tac\n"); (!tac ~status:(proof,goal)) ;; let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);; -