From 11ca3113365639136cf65a74c345080a9434e69b Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 27 Sep 2013 19:20:27 +0000 Subject: Removing a bunch of generic equalities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/syntax/ascii_syntax.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins/syntax/ascii_syntax.ml') diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 180d15009..790e1970b 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -35,17 +35,17 @@ open Lazy let interp_ascii dloc p = let rec aux n p = - if n = 0 then [] else + if Int.equal n 0 then [] else let mp = p mod 2 in - GRef (dloc,if mp = 0 then glob_false else glob_true) + GRef (dloc,if Int.equal mp 0 then glob_false else glob_true) :: (aux (n-1) (p/2)) in GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p) let interp_ascii_string dloc s = let p = - if String.length s = 1 then int_of_char s.[0] + if Int.equal (String.length s) 1 then int_of_char s.[0] else - if String.length s = 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] + if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] then int_of_string s else user_err_loc (dloc,"interp_ascii_string", @@ -54,13 +54,13 @@ let interp_ascii_string dloc s = let uninterp_ascii r = let rec uninterp_bool_list n = function - | [] when n = 0 -> 0 - | GRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | GRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l) + | [] when Int.equal n 0 -> 0 + | GRef (_,k)::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | GRef (_,k)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try let aux = function - | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l + | GApp (_,GRef (_,k),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with -- cgit v1.2.3