From c290236ef8e2a2310e10d807a3f852c33e6bd919 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Oct 2002 08:27:21 +0000 Subject: [PATCH] Now esempi/fourier.cic end with a proof! - used change_tac to change from a->False to ~a just before tac2. Fix: Ad hoc change_tac may not work sometimes. check what Cic.Anonimous means. --- helm/gTopLevel/fourierR.ml | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 0dd76f89a..c23cc448d 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -726,8 +726,8 @@ let tac_zero_inf_false gl (n,d) ~status= 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"); + 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 @@ -1157,6 +1157,9 @@ theoreme,so let's parse our thesis *) 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"); + PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status) ~continuation:(Tacticals.then_ @@ -1192,7 +1195,7 @@ theoreme,so let's parse our thesis *) 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 + let r = PrimitiveTactics.apply_tac ~term:_sym_eqT ~status in debug("fine ECCOCI\n"); r) @@ -1206,8 +1209,25 @@ theoreme,so let's parse our thesis *) r) ; "id", Ring.id_tac] ]) -(* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *) - ;tac2])) + ;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 = + (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:tac2])) ;!tac1]);(*end tac:=*) tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False) -- 2.39.2