Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est de toutes façons inutile)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5733 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 4 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 110a64a058..e736edeffb 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -791,7 +791,7 @@ let rec scalar p n = function
   | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
   | (Oatom _ as t) -> [], Otimes(t,Oz n)
   | Oz i -> [focused_simpl p],Oz(n*i)
-  | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n |]))
+  | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |]))
       
 let rec scalar_norm p_init = 
   let rec loop p = function
@@ -1409,7 +1409,14 @@ let coq_omega gl =
   end
 
 let coq_omega = solver_time coq_omega
-		  
+
+let rec is_nat_constant t =
+  match destructurate_term t with
+  | Kapp((Plus|Mult|Minus),[t1;t2]) -> is_nat_constant t1 & is_nat_constant t2
+  | Kapp((S|Pred),[t]) -> is_nat_constant t
+  | Kapp(O,[]) -> true
+  | _ -> false
+
 let nat_inject gl =
   let aux = id_of_string "auxiliary" in
   let table = Hashtbl.create 7 in
@@ -1422,7 +1429,7 @@ let nat_inject gl =
 	    (explore (P_APP 1 :: p) t1);
 	    (explore (P_APP 2 :: p) t2)
           ]
-      | Kapp(Mult,[t1;t2]) ->
+      | Kapp(Mult,[t1;t2]) when is_nat_constant t1 or is_nat_constant t2 ->
           tclTHENLIST [
 	    (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
               ((Lazy.force coq_inj_mult),[t1;t2]));
@@ -1528,7 +1535,7 @@ let nat_inject gl =
 		  (explore [P_APP 2; P_TYPE] t2);
 		  (reintroduce i);
 		  (loop lit)
-]
+                ]
             | Kapp(Eq,[typ;t1;t2]) ->
 		if pf_conv_x gl typ (Lazy.force coq_nat) then
                   tclTHENLIST [