From 7da3e3d85c88eb42e932230048cb0db255474b5d Mon Sep 17 00:00:00 2001 From: fbesson Date: Fri, 20 May 2011 17:01:54 +0000 Subject: added support to handle division by a constant over R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14147 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/certificate.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/micromega/certificate.ml') diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 6e8018b91..5efe9f426 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -43,7 +43,7 @@ let z_spec = { number_to_num = (fun x -> Big_int (C2Ml.z_big_int x)); zero = Mc.Z0; unit = Mc.Zpos Mc.XH; - mult = Mc.zmult; + mult = Mc.Z.mul; eqb = Mc.zeq_bool } @@ -579,7 +579,7 @@ let q_cert_of_pos pos = | Sub(t1,t2) -> PEsub (term_to_z_expr t1, term_to_z_expr t2) | _ -> failwith "term_to_z_expr: not implemented" - let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.zplus Mc.zmult Mc.zminus Mc.zopp Mc.zeq_bool (term_to_z_expr e) + let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.Z.add Mc.Z.mul Mc.Z.sub Mc.Z.opp Mc.zeq_bool (term_to_z_expr e) let z_cert_of_pos pos = let s,pos = (scale_certificate pos) in -- cgit v1.2.3