From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 16 Oct 2002 14:21:06 +0000 (+0000)
Subject: - write_tac fixed (the list of new goals was empty)
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~29
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c14d84b2a11e8505fc9b0b8a1db4bb41c90de1e1;p=helm.git

- write_tac fixed (the list of new goals was empty)
- some new bugs introduced here and there ;-)
---

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index c46973e2c..566003e89 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -68,10 +68,15 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
     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)
+    
+     let (proof',goals) =
+      PrimitiveTactics.exact_tac  
+       ~term:(C.Appl 
+         [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
+        ~status:((curi,metasenv',pbo,pty),goal)
+     in
+      assert (List.length goals = 0) ;
+      (proof',[fresh_meta])
 ;;
 
 (******************** THE FOURIER TACTIC ***********************)
@@ -520,7 +525,7 @@ let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_ut
 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 _sym_eqT = Cic.Const(UriManager.uri_of_string "/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
+let _sym_eqT = Cic.Const(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
 (*****************************************************************************************************)
 let is_int x = (x.den)=1
 ;;
@@ -1036,21 +1041,27 @@ let rec fourier ~status:(s_proof,s_goal)=
 						~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
 			    	~continuation:(Tacticals.thens 
 						~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
-		 	       			~continuations:[tac2;(Tacticals.thens 
+		 	       			~continuations:[(*tac2;*)(Tacticals.thens 
 							~start:(equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
 							~continuations:   
-(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... 	*)
-					[Tacticals.try_tactics 
-						(* ???????????????????????????? *)
-						~tactics:[ "ring", Ring.ring_tac  ; "id", Ring.id_tac] 
-					;
-					Tacticals.then_ 
-						~start:(PrimitiveTactics.apply_tac ~term:_sym_eqT)
-				      		~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
-					]
+		[
+		(*
+		Tacticals.try_tactics 
+			(* ???????????????????????????? *)
+		~tactics:[ "ring", Ring.ring_tac  ; "id", Ring.id_tac] 
+				;*)
+		Tacticals.then_ 
+		~start:(PrimitiveTactics.apply_tac ~term:_sym_eqT)
+	      	~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
+		;
+		Tacticals.try_tactics 
+			(* ???????????????????????????? *)
+		~tactics:[ "ring", Ring.ring_tac  ; "id", Ring.id_tac] 
+		
+		]
                                
 					 )
-						] (* end continuations before comment *)
+					;tac2	] (* end continuations before comment *)
 					)
 				);
                        !tac1]