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.

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 0dd76f89a5a806ade2c9556b3226639014b053f5..c23cc448ddf4e826816931608f93035aa99fc82d 100644 (file)
--- 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)