diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-05-28 14:36:51 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-05-28 14:36:51 +0000 |
| commit | 5b461bf82826dec5aee1ab51af87dfe684b41f88 (patch) | |
| tree | ebd66dbf4345e155ebb91b48493ff9a0ae07d32e /contrib | |
| parent | 2e5f138018dc3e57686b06f5715ef065e6ca2879 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index e736edeff..3c41007ef 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])); |