X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=a4630ab7aca1e47db84676838ceaead5d6ffb742;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=744a86e6704831b8e75f68e0e98f59c78e283636;hpb=fe07fcacb7060dddc6542b04bc1168f444ceaebf;p=helm.git diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 744a86e67..a4630ab7a 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -31,7 +31,9 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = 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 = + + prerr_endline("rewrite chiamata con "^CicPp.ppterm gty^"\n"); + 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") -> @@ -79,6 +81,37 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); (proof',[fresh_meta]) ;; +(* ti ho beccato !!!!!!!!!! qui' salta fuori un or. perche'?*) + + + +let simpl_tac ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + +prerr_endline("simpl_tac su "^CicPp.ppterm ty); + + let new_ty = ProofEngineReduction.simpl context ty in + +prerr_endline("ritorna "^CicPp.ppterm new_ty); + + let new_metasenv = + List.map + (function + (n,_,_) when n = metano -> (metano,context,new_ty) + | _ as t -> t + ) metasenv + in + (curi,new_metasenv,pbo,pty), [metano] + +;; + +let rewrite_simpl_tac ~term ~status = + + Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status + +;; + (******************** THE FOURIER TACTIC ***********************) (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients @@ -362,6 +395,7 @@ type hineq={hname:Cic.term; (* le nom de l'hypoth *) let ineq1_of_term (h,t) = + debug("Trasformo in ineq "^CicPp.ppterm t^"\n"); match t with (* match t *) Cic.Appl (t1::next) -> let arg1= List.hd next in @@ -378,7 +412,7 @@ let ineq1_of_term (h,t) = (flin_of_term arg2); hstrict=true}] |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> - [{hname=h; + [{hname=h; htype="Rgt"; hleft=arg2; hright=arg1; @@ -386,7 +420,7 @@ let ineq1_of_term (h,t) = (flin_of_term arg1); hstrict=true}] |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> - [{hname=h; + [{hname=h; htype="Rle"; hleft=arg1; hright=arg2; @@ -394,7 +428,7 @@ let ineq1_of_term (h,t) = (flin_of_term arg2); hstrict=false}] |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> - [{hname=h; + [{hname=h; htype="Rge"; hleft=arg2; hright=arg1; @@ -404,14 +438,16 @@ let ineq1_of_term (h,t) = |_->assert false)(* match u *) | Cic.MutInd (u,i,o) -> (match UriManager.string_of_uri u with - "cic:/Coq/Init/Logic_Type/eqT.con" -> - let t0= arg1 in + "cic:/Coq/Init/Logic_Type/eqT.ind" -> + debug("Ho trovato una ==\n"); + let t0= arg1 in let arg1= arg2 in let arg2= List.hd(List.tl (List.tl next)) in (match t0 with Cic.Const (u,boh) -> (match UriManager.string_of_uri u with "cic:/Coq/Reals/Rdefinitions/R.con"-> + [{hname=h; htype="eqTLR"; hleft=arg1; @@ -426,11 +462,11 @@ let ineq1_of_term (h,t) = hflin= flin_minus (flin_of_term arg2) (flin_of_term arg1); hstrict=false}] - |_-> assert false) - |_-> assert false) - |_-> assert false) - |_-> assert false)(* match t1 *) - |_-> assert false (* match t *) + |_-> debug("eqT deve essere applicato a const R\n");assert false) + |_-> debug("eqT deve essere appl a const\n");assert false) + |_-> debug("Il trmine e' un appl mutind ma non eqT\n");assert false) + |_-> debug("Il termine non e' una app di const o app di mutind\n");assert false)(* match t1 *) + |_-> debug("Il termine non e' una applicazione\n");assert false (* match t *) ;; (* coq wrapper let ineq1_of_constr = ineq1_of_term;; @@ -687,28 +723,23 @@ let tac_zero_infeq_pos gl (n,d) ~status = *) let tac_zero_inf_false gl (n,d) ~status= -debug("inizio tac_zero_inf_false\n"); + debug("inizio tac_zero_inf_false\n"); if n=0 then - (debug "1\n";let r = (PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in + (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in debug("fine\n"); r) else (debug "2\n";let r = (Tacticals.then_ ~start:( - fun ~status:(proof,goal as status) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - - debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with " - ^ CicPp.ppterm ty ^"\n"); - - let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in - - debug("!!!!!!!!!2\n"); - r - - ) - - ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in + fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + debug("!!!!!!!!1:unify "^CicPp.ppterm _Rle_not_lt^" with " + ^ CicPp.ppterm ty ^" fails\n"); + let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in + debug("!!!!!!!!!2\n"); + r + ) + ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in debug("fine\n"); r ) @@ -717,13 +748,19 @@ debug("inizio tac_zero_inf_false\n"); (* preuve que 0<=(-n)*(1/d) => False *) -let tac_zero_infeq_false gl (n,d) ~status= -debug("stat tac_zero_infeq_false"); -let r = - (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) +let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)= +debug("stat tac_zero_infeq_false\n"); +(*let r = + ( + let curi,metasenv,pbo,pty = proof in + let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + + debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); + Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) ~continuation:(tac_zero_inf_pos (-n,d))) ~status in - debug("stat tac_zero_infeq_false"); - r + debug("end tac_zero_infeq_false\n"); + r*) + Ring.id_tac ~status ;; @@ -877,13 +914,14 @@ debug("inizio EQ\n"); let irl = ProofEngineHelpers.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in -debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); +debug("chamo rewrite tac su "^CicPp.ppterm (C.Meta (fresh_meta,irl))^" e ty "^CicPp.ppterm ty ^"\n"); let (proof,goals) = - rewrite_tac ~term:(C.Meta (fresh_meta,irl)) + rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ~status:((curi,metasenv',pbo,pty),goal) in let new_goals = fresh_meta::goals in -debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "^string_of_int( List.length goals)^"+ meta\n"); +debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " + ^string_of_int( List.length goals)^"+ meta\n"); (proof,new_goals) ;; @@ -900,9 +938,9 @@ let assumption_tac ~status:(proof,goal)= let num = ref 0 in let tac_list = List.map ( fun x -> num := !num + 1; - match x with - Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) - | _ -> ("fake",tcl_fail 1) + match x with + Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) + | _ -> ("fake",tcl_fail 1) ) context in @@ -985,7 +1023,7 @@ theoreme,so let's parse our thesis *) (* transform hyps into inequations *) List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) - with _-> ()) + with _-> debug("Impossibile trasformare l'ipotesi "^CicPp.ppterm (snd h)^" in ineq\n");) hyps; @@ -996,7 +1034,7 @@ theoreme,so let's parse our thesis *) let tac=ref Ring.id_tac in if res=[] then (print_string "Tactic Fourier fails.\n";flush stdout; - failwith "fourier_tac fails") + failwith "fourier can't proove it") else ( match res with (*match res*) @@ -1021,17 +1059,16 @@ theoreme,so let's parse our thesis *) (* on construit la combinaison linéaire des inéquation *) (match (!lutil) with (*match (!lutil) *) - (h1,c1)::lutil -> - - debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n"; + (h1,c1)::lutil -> + debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n"; - let s=ref (h1.hstrict) in + let s=ref (h1.hstrict) in - let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in - let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in + let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in + let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in - List.iter (fun (h,c) -> + List.iter (fun (h,c) -> s:=(!s)||(h.hstrict); t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl [_Rmult;rational_to_real c;h.hleft ] ]); @@ -1039,219 +1076,188 @@ theoreme,so let's parse our thesis *) [_Rmult;rational_to_real c;h.hright] ])) lutil; - let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in - let tc=rational_to_real cres in + let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in + let tc=rational_to_real cres in (* 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 ( 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 (rational_to_fraction c1)] ~status)) - - in - s:=h1.hstrict; + debug "inizio a costruire tac1\n"; + Fourier.print_rational(c1); - 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) - ~continuations:[!tac1;tac_use h; - tac_zero_inf_pos - (rational_to_fraction c)])) - else - ( - 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 (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 - (rational_to_fraction c)])) - else - ( - debug("tac1 4\n"); - tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) - ~continuations:[!tac1;tac_use h; - tac_zero_inf_pos - (rational_to_fraction c)])) - - ) - ); - s:=(!s)||(h.hstrict)) - lutil;(*end List.iter*) + let tac1=ref ( fun ~status -> + 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 + (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) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + else + (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 + (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 + (rational_to_fraction c)]) + ) + else + (debug("tac1 4\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + ) + ); + s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) + + let tac2 = + if sres then + tac_zero_inf_false goal (rational_to_fraction cres) + else + tac_zero_infeq_false goal (rational_to_fraction cres) + in + tac:=(Tacticals.thens + ~start:(my_cut ~term:ineq) + ~continuations:[Tacticals.then_ + ~start:(fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) + metasenv in + + debug("Change_tac "^CicPp.ppterm ty^" with "^CicPp.ppterm (Cic.Appl [ _not; ineq]) ^"\n"); - let tac2= if sres then - tac_zero_inf_false goal (rational_to_fraction cres) - else - tac_zero_infeq_false goal (rational_to_fraction cres) - in - tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) - ~continuations:[Tacticals.then_ (* ?????????????????????????????? *) - ~start:(fun ~status:(proof,goal as status) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status) - ~continuation:(Tacticals.then_ - ~start:(PrimitiveTactics.apply_tac - ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le)) - ~continuation:(Tacticals.thens - ~start:( - - fun ~status -> - let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc ~status - in - (match r with (p,gl) -> - debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); - - r - - ) - ~continuations:[(*tac2;*)(Tacticals.thens - ~start:( - fun ~status -> - let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in - (match r with (p,gl) -> - debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));r - - ) - ~continuations: - (* ******* *) - [ - Tacticals.then_ - ~start:( - fun ~status:(proof,goal as status) -> - debug("ECCOCI\n"); - - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - - debug("ty = "^CicPp.ppterm ty^"\n"); - - let r = PrimitiveTactics.apply_tac ~term:_sym_eqT ~status in - debug("fine ECCOCI\n"); - r - ) - ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1) - - - ; - Tacticals.try_tactics - (* ???????????????????????????? *) - ~tactics:[ "ring", - - (fun ~status -> - debug("begin RING\n"); - let r = Ring.ring_tac ~status in - debug ("end RING\n"); - r) - - - ; "id", Ring.id_tac] - - ] - - );tac2(* < order *) - ] (* end continuations before comment *) - ) - ); - !tac1] - );(*end tac:=*) - tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False) - ~continuations:[Tacticals.then_ - (* ??????????????????????????????? - in coq era intro *) - ~start:(PrimitiveTactics.intros_tac ~name:"??") - (* ????????????????????????????? *) - - ~continuation:contradiction_tac;!tac]) - - - |_-> assert false)(*match (!lutil) *) + PrimitiveTactics.change_tac ~what:ty + ~with_what:(Cic.Appl [ _not; ineq]) ~status) + ~continuation:(Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term: + (if sres then _Rnot_lt_lt else _Rnot_le_le)) + ~continuation:(Tacticals.thens + ~start:( + fun ~status -> + let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc + ~status + in + (match r with (p,gl) -> + debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); + r) + ~continuations:[(Tacticals.thens + ~start:( + fun ~status:(proof,goals as status) -> + + let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in + (match r with (p,gl) -> + debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); + r) + ~continuations: + [PrimitiveTactics.apply_tac ~term:_Rinv_R1 +(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno + di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i + parametri della equality_replace vengono passati al contrario? Oppure la + tattica usa i parametri al contrario? + ~continuations:[Tacticals.then_ + ~start:( + fun ~status:(proof,goal as status) -> + debug("ECCOCI\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m= + goal) metasenv in + debug("ty = "^CicPp.ppterm ty^"\n"); + let r = PrimitiveTactics.apply_tac ~term:_sym_eqT + ~status in + debug("fine ECCOCI\n"); + r) + ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1) +*) + ;Tacticals.try_tactics + ~tactics:[ "ring", (fun ~status -> + debug("begin RING\n"); + let r = Ring.ring_tac ~status in + debug ("end RING\n"); + r) + ; "id", Ring.id_tac] + ]) + ;Tacticals.then_ + ~start: + ( + fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m= + goal) metasenv in + (* check if ty is of type *) + let w1 = + debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n"); + (match ty with + (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*) + Cic.Prod (Cic.Anonimous,a,b) -> (Cic.Appl [_not;a]) + |_ -> assert false) + in + let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in + debug("fine MY_CHNGE\n"); + r + ) + ~continuation:Ring.id_tac(*tac2*)])) + ;Ring.id_tac(*!tac1*)]);(*end tac:=*) + tac:=(Tacticals.thens + ~start:(PrimitiveTactics.cut_tac ~term:_False) + ~continuations:[Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ~name:"??") + ~continuation:contradiction_tac + ;!tac]) + + + |_-> assert false)(*match (!lutil) *) |_-> assert false); (*match res*) - debug ("finalmente applico tac\n"); (!tac ~status:(proof,goal)) - ;; let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);; -let simpl_tac ~status:(proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - -prerr_endline("simpl_tac su "^CicPp.ppterm ty); - - let new_ty = ProofEngineReduction.simpl context ty in - -prerr_endline("ritorna "^CicPp.ppterm new_ty); - - let new_metasenv = - List.map - (function - (n,_,_) when n = metano -> (metano,context,new_ty) - | _ as t -> t - ) metasenv - in - (curi,new_metasenv,pbo,pty), [metano] - -;; - -let rewrite_simpl_tac ~term ~status = - - Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status - -;;