Skip to content
Browse files

Removing generic equality in Syntax plugin.

  • Loading branch information...
1 parent 26f47b0 commit 412f848e681e3c94c635f65638310a13d675449e @ppedrot ppedrot committed Mar 2, 2014
Showing with 14 additions and 14 deletions.
  1. +1 −1 interp/notation_ops.ml
  2. +2 −2 plugins/syntax/nat_syntax.ml
  3. +9 −9 plugins/syntax/numbers_syntax.ml
  4. +2 −2 plugins/syntax/string_syntax.ml
View
2 interp/notation_ops.ml
@@ -473,7 +473,7 @@ let rec subst_notation_constr subst bound raw =
| _ -> knd
in
let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in
- if nsolve == solve && nknd = knd then raw
+ if nsolve == solve && nknd == knd then raw
else NHole (nknd, nsolve)
| NCast (r1,k) ->
View
4 plugins/syntax/nat_syntax.ml
@@ -50,8 +50,8 @@ let nat_of_int dloc n =
exception Non_closed_number
let rec int_of_nat = function
- | GApp (_,GRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
- | GRef (_,z) when z = glob_O -> zero
+ | GApp (_,GRef (_,s),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
+ | GRef (_,z) when Globnames.eq_gr z glob_O -> zero
| _ -> raise Non_closed_number
let uninterp_nat p =
View
18 plugins/syntax/numbers_syntax.ml
@@ -110,12 +110,12 @@ let bigint_of_int31 =
let rec args_parsing args cur =
match args with
| [] -> cur
- | (GRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur)
- | (GRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur))
+ | (GRef (_,b))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
+ | (GRef (_,b))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
| _ -> raise Non_closed
in
function
- | GApp (_, GRef (_, c), args) when c=int31_construct -> args_parsing args zero
+ | GApp (_, GRef (_, c), args) when eq_gr c int31_construct -> args_parsing args zero
| _ -> raise Non_closed
let uninterp_int31 i =
@@ -199,14 +199,14 @@ let interp_bigN dloc n =
let bigint_of_word =
let rec get_height rc =
match rc with
- | GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
+ | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW ->
1+max (get_height lft) (get_height rght)
| _ -> 0
in
let rec transform hght rc =
match rc with
- | GApp (_,GRef(_,c),_) when c = zn2z_W0-> zero
- | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW->
+ | GApp (_,GRef(_,c),_) when eq_gr c zn2z_W0-> zero
+ | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW->
let new_hght = hght-1 in
add (mult (rank new_hght)
(transform new_hght lft))
@@ -262,8 +262,8 @@ let interp_bigZ dloc n =
(* pretty printing functions for bigZ *)
let bigint_of_bigZ = function
- | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
- | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_neg ->
+ | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
+ | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_neg ->
let opp_val = bigint_of_bigN one_arg in
if equal opp_val zero then
raise Non_closed
@@ -294,7 +294,7 @@ let interp_bigQ dloc n =
let uninterp_bigQ rc =
try match rc with
- | GApp (_, GRef(_,c), [one_arg]) when c = bigQ_z ->
+ | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigQ_z ->
Some (bigint_of_bigZ one_arg)
| _ -> None (* we don't pretty-print yet fractions *)
with Non_closed -> None
View
4 plugins/syntax/string_syntax.ml
@@ -41,11 +41,11 @@ let uninterp_string r =
try
let b = Buffer.create 16 in
let rec aux = function
- | GApp (_,GRef (_,k),[a;s]) when k = force glob_String ->
+ | GApp (_,GRef (_,k),[a;s]) when eq_gr k (force glob_String) ->
(match uninterp_ascii a with
| Some c -> Buffer.add_char b (Char.chr c); aux s
| _ -> raise Non_closed_string)
- | GRef (_,z) when z = force glob_EmptyString ->
+ | GRef (_,z) when eq_gr z (force glob_EmptyString) ->
Some (Buffer.contents b)
| _ ->
raise Non_closed_string

0 comments on commit 412f848

Please sign in to comment.
Something went wrong with that request. Please try again.