aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/syntax/ascii_syntax.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-27 19:20:27 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-27 19:20:27 +0000
commit11ca3113365639136cf65a74c345080a9434e69b (patch)
treeda263c149cd1e90bde14768088730e48e78e4776 /plugins/syntax/ascii_syntax.ml
parentee2f85396fa0cef65bc4295b5ac6c259e83df134 (diff)
Removing a bunch of generic equalities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/ascii_syntax.ml')
-rw-r--r--plugins/syntax/ascii_syntax.ml16
1 files changed, 8 insertions, 8 deletions
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