From 1d2bd140d14561951f8214edf15abe4f40dcb649 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 11 Oct 2002 15:24:56 +0000 Subject: [PATCH] - idtac used for debugging removed - bug fixed: the natural number 1 was mapped to (Rplus R1 R0). It is now mapped to R1 (as it should be). This close all the residual bugs. Still to do: we need to close the last open branch using equality_replace, as soon as it is implemented. --- helm/gTopLevel/fourierR.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 0998a37d0..1de87fdd9 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -483,6 +483,7 @@ let rec rational_to_fraction x= (x.num,x.den) let rec int_to_real_aux n = match n with 0 -> _R0 (* o forse R0 + R0 ????? *) + | 1 -> _R1 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ] ;; @@ -906,9 +907,7 @@ let rec fourier ~status:(s_proof,s_goal)= PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) ~continuations:[tac_use h1; - Ring.id_tac] ~status - - (*tac_zero_inf_pos (rational_to_fraction c1)] ~status*) + tac_zero_inf_pos (rational_to_fraction c1)] ~status ) else @@ -945,9 +944,7 @@ let rec fourier ~status:(s_proof,s_goal)= ) ~continuations:[!tac1;tac_use h; - Ring.id_tac - (*tac_zero_inf_pos - (rational_to_fraction c)*) + tac_zero_inf_pos (rational_to_fraction c) ])) ) -- 2.39.2