From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 25 Oct 2002 08:27:21 +0000 (+0000)
Subject: Now esempi/fourier.cic end with a proof!
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c290236ef8e2a2310e10d807a3f852c33e6bd919;p=helm.git

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 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)