From 5b461bf82826dec5aee1ab51af87dfe684b41f88 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 28 May 2004 14:36:51 +0000
Subject: Retour sur amendement de l'interprétation mult sur nat (bug 743) car
 incompatible avec la sémantique précédente qui identifiait "Z_of_nat x *
 Z_of_nat y" avec "Z_of_nat (x * y)"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5774 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/coq_omega.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index e736edeffb..3c41007ef7 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1410,13 +1410,6 @@ let coq_omega gl =
 
 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
@@ -1429,7 +1422,7 @@ let nat_inject gl =
 	    (explore (P_APP 1 :: p) t1);
 	    (explore (P_APP 2 :: p) t2)
           ]
-      | Kapp(Mult,[t1;t2]) when is_nat_constant t1 or is_nat_constant t2 ->
+      | Kapp(Mult,[t1;t2]) ->
           tclTHENLIST [
 	    (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
               ((Lazy.force coq_inj_mult),[t1;t2]));
-- 
cgit v1.2.3