diff options
Diffstat (limited to 'plugins/syntax/r_syntax.ml')
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index efbd140ee..545f205db 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -55,7 +55,7 @@ let r_of_posint dloc n = let (q,r) = div2_with_rest n in let b = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in - if n <> zero then r_of_pos n else GRef(dloc,glob_R0) + if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0) let r_of_int dloc z = if is_strictly_neg z then @@ -72,34 +72,34 @@ let bignat_of_r = let rec bignat_of_pos = function (* 1+1 *) | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)]) - when p = glob_Rplus && o1 = glob_R1 && o2 = glob_R1 -> two + when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two (* 1+(1+1) *) | GApp (_,GRef (_,p1), [GRef (_,o1); GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])]) - when p1 = glob_Rplus && p2 = glob_Rplus && - o1 = glob_R1 && o2 = glob_R1 && o3 = glob_R1 -> three + when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus && + Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three (* (1+1)*b *) - | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult -> - if bignat_of_pos a <> two then raise Non_closed_number; + | GApp (_,GRef (_,p), [a; b]) when Globnames.eq_gr p glob_Rmult -> + if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; mult_2 (bignat_of_pos b) (* 1+(1+1)*b *) | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])]) - when p1 = glob_Rplus && p2 = glob_Rmult && o = glob_R1 -> - if bignat_of_pos a <> two then raise Non_closed_number; + when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1 -> + if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; add_1 (mult_2 (bignat_of_pos b)) | _ -> raise Non_closed_number in let bignat_of_r = function - | GRef (_,a) when a = glob_R0 -> zero - | GRef (_,a) when a = glob_R1 -> one + | GRef (_,a) when Globnames.eq_gr a glob_R0 -> zero + | GRef (_,a) when Globnames.eq_gr a glob_R1 -> one | r -> bignat_of_pos r in bignat_of_r let bigint_of_r = function - | GApp (_,GRef (_,o), [a]) when o = glob_Ropp -> + | GApp (_,GRef (_,o), [a]) when Globnames.eq_gr o glob_Ropp -> let n = bignat_of_r a in - if n = zero then raise Non_closed_number; + if Bigint.equal n zero then raise Non_closed_number; neg n | a -> bignat_of_r a |