aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/ascii_syntax.ml12
-rw-r--r--plugins/syntax/nat_syntax.ml12
-rw-r--r--plugins/syntax/numbers_syntax.ml64
-rw-r--r--plugins/syntax/r_syntax.ml38
-rw-r--r--plugins/syntax/string_syntax.ml12
-rw-r--r--plugins/syntax/z_syntax.ml50
6 files changed, 94 insertions, 94 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 79e1a6eb2..50498f0f4 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -39,9 +39,9 @@ let interp_ascii dloc p =
let rec aux n p =
if n = 0 then [] else
let mp = p mod 2 in
- RRef (dloc,if mp = 0 then glob_false else glob_true)
+ GRef (dloc,if mp = 0 then glob_false else glob_true)
:: (aux (n-1) (p/2)) in
- RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p)
+ GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p)
let interp_ascii_string dloc s =
let p =
@@ -57,12 +57,12 @@ let interp_ascii_string dloc s =
let uninterp_ascii r =
let rec uninterp_bool_list n = function
| [] when n = 0 -> 0
- | RRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l)
- | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
+ | 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)
| _ -> raise Non_closed_ascii in
try
let rec aux = function
- | RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
+ | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
| _ -> raise Non_closed_ascii in
Some (aux r)
with
@@ -78,4 +78,4 @@ let _ =
Notation.declare_string_interpreter "char_scope"
(ascii_path,ascii_module)
interp_ascii_string
- ([RRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)
+ ([GRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index b673fdb9d..3d8860be4 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -36,11 +36,11 @@ let nat_of_int dloc n =
strbrk "working with large numbers in nat (observed threshold " ++
strbrk "may vary from 5000 to 70000 depending on your system " ++
strbrk "limits and on the command executed).");
- let ref_O = RRef (dloc, glob_O) in
- let ref_S = RRef (dloc, glob_S) in
+ let ref_O = GRef (dloc, glob_O) in
+ let ref_S = GRef (dloc, glob_S) in
let rec mk_nat acc n =
if n <> zero then
- mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n)
+ mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n)
else
acc
in
@@ -56,8 +56,8 @@ let nat_of_int dloc n =
exception Non_closed_number
let rec int_of_nat = function
- | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
- | RRef (_,z) when z = glob_O -> zero
+ | GApp (_,GRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
+ | GRef (_,z) when z = glob_O -> zero
| _ -> raise Non_closed_number
let uninterp_nat p =
@@ -73,4 +73,4 @@ let _ =
Notation.declare_numeral_interpreter "nat_scope"
(nat_path,["Coq";"Init";"Datatypes"])
nat_of_int
- ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, true)
+ ([GRef (dummy_loc,glob_S); GRef (dummy_loc,glob_O)], uninterp_nat, true)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 2a0425dca..892a5595a 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -98,9 +98,9 @@ exception Non_closed
(* parses a *non-negative* integer (from bigint.ml) into an int31
wraps modulo 2^31 *)
let int31_of_pos_bigint dloc n =
- let ref_construct = RRef (dloc, int31_construct) in
- let ref_0 = RRef (dloc, int31_0) in
- let ref_1 = RRef (dloc, int31_1) in
+ let ref_construct = GRef (dloc, int31_construct) in
+ let ref_0 = GRef (dloc, int31_0) in
+ let ref_1 = GRef (dloc, int31_1) in
let rec args counter n =
if counter <= 0 then
[]
@@ -108,7 +108,7 @@ let int31_of_pos_bigint dloc n =
let (q,r) = div2_with_rest n in
(if r then ref_1 else ref_0)::(args (counter-1) q)
in
- RApp (dloc, ref_construct, List.rev (args 31 n))
+ GApp (dloc, ref_construct, List.rev (args 31 n))
let error_negative dloc =
Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
@@ -125,12 +125,12 @@ let bigint_of_int31 =
let rec args_parsing args cur =
match args with
| [] -> cur
- | (RRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur)
- | (RRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 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))
| _ -> raise Non_closed
in
function
- | RApp (_, RRef (_, c), args) when c=int31_construct -> args_parsing args zero
+ | GApp (_, GRef (_, c), args) when c=int31_construct -> args_parsing args zero
| _ -> raise Non_closed
let uninterp_int31 i =
@@ -143,7 +143,7 @@ let uninterp_int31 i =
let _ = Notation.declare_numeral_interpreter int31_scope
(int31_path, int31_module)
interp_int31
- ([RRef (Util.dummy_loc, int31_construct)],
+ ([GRef (Util.dummy_loc, int31_construct)],
uninterp_int31,
true)
@@ -174,24 +174,24 @@ let height bi =
(* n must be a non-negative integer (from bigint.ml) *)
let word_of_pos_bigint dloc hght n =
- let ref_W0 = RRef (dloc, zn2z_W0) in
- let ref_WW = RRef (dloc, zn2z_WW) in
+ let ref_W0 = GRef (dloc, zn2z_W0) in
+ let ref_WW = GRef (dloc, zn2z_WW) in
let rec decomp hgt n =
if is_neg_or_zero hgt then
int31_of_pos_bigint dloc n
else if equal n zero then
- RApp (dloc, ref_W0, [RHole (dloc, Evd.InternalHole)])
+ GApp (dloc, ref_W0, [GHole (dloc, Evd.InternalHole)])
else
let (h,l) = split_at hgt n in
- RApp (dloc, ref_WW, [RHole (dloc, Evd.InternalHole);
+ GApp (dloc, ref_WW, [GHole (dloc, Evd.InternalHole);
decomp (sub_1 hgt) h;
decomp (sub_1 hgt) l])
in
decomp hght n
let bigN_of_pos_bigint dloc n =
- let ref_constructor i = RRef (dloc, bigN_constructor i) in
- let result h word = RApp (dloc, ref_constructor h, if less_than h n_inlined then
+ let ref_constructor i = GRef (dloc, bigN_constructor i) in
+ let result h word = GApp (dloc, ref_constructor h, if less_than h n_inlined then
[word]
else
[Nat_syntax.nat_of_int dloc (sub h n_inlined);
@@ -215,7 +215,7 @@ let interp_bigN dloc n =
let bigint_of_word =
let rec get_height rc =
match rc with
- | RApp (_,RRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
+ | GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
let hleft = get_height lft in
let hright = get_height rght in
add_1
@@ -227,8 +227,8 @@ let bigint_of_word =
in
let rec transform hght rc =
match rc with
- | RApp (_,RRef(_,c),_) when c = zn2z_W0-> zero
- | RApp (_,RRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in
+ | GApp (_,GRef(_,c),_) when c = zn2z_W0-> zero
+ | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in
add (mult (rank new_hght)
(transform (new_hght) lft))
(transform (new_hght) rght)
@@ -240,8 +240,8 @@ let bigint_of_word =
let bigint_of_bigN rc =
match rc with
- | RApp (_,_,[one_arg]) -> bigint_of_word one_arg
- | RApp (_,_,[_;second_arg]) -> bigint_of_word second_arg
+ | GApp (_,_,[one_arg]) -> bigint_of_word one_arg
+ | GApp (_,_,[_;second_arg]) -> bigint_of_word second_arg
| _ -> raise Non_closed
let uninterp_bigN rc =
@@ -257,7 +257,7 @@ let uninterp_bigN rc =
let bigN_list_of_constructors =
let rec build i =
if less_than i (add_1 n_inlined) then
- RRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i))
+ GRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i))
else
[]
in
@@ -274,17 +274,17 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
(*** Parsing for bigZ in digital notation ***)
let interp_bigZ dloc n =
- let ref_pos = RRef (dloc, bigZ_pos) in
- let ref_neg = RRef (dloc, bigZ_neg) in
+ let ref_pos = GRef (dloc, bigZ_pos) in
+ let ref_neg = GRef (dloc, bigZ_neg) in
if is_pos_or_zero n then
- RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
+ GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
else
- RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])
+ GApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])
(* pretty printing functions for bigZ *)
let bigint_of_bigZ = function
- | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
- | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_neg ->
+ | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
+ | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_neg ->
let opp_val = bigint_of_bigN one_arg in
if equal opp_val zero then
raise Non_closed
@@ -303,19 +303,19 @@ let uninterp_bigZ rc =
let _ = Notation.declare_numeral_interpreter bigZ_scope
(bigZ_path, bigZ_module)
interp_bigZ
- ([RRef (Util.dummy_loc, bigZ_pos);
- RRef (Util.dummy_loc, bigZ_neg)],
+ ([GRef (Util.dummy_loc, bigZ_pos);
+ GRef (Util.dummy_loc, bigZ_neg)],
uninterp_bigZ,
true)
(*** Parsing for bigQ in digital notation ***)
let interp_bigQ dloc n =
- let ref_z = RRef (dloc, bigQ_z) in
- RApp (dloc, ref_z, [interp_bigZ dloc n])
+ let ref_z = GRef (dloc, bigQ_z) in
+ GApp (dloc, ref_z, [interp_bigZ dloc n])
let uninterp_bigQ rc =
try match rc with
- | RApp (_, RRef(_,c), [one_arg]) when c = bigQ_z ->
+ | GApp (_, GRef(_,c), [one_arg]) when c = bigQ_z ->
Some (bigint_of_bigZ one_arg)
| _ -> None (* we don't pretty-print yet fractions *)
with Non_closed -> None
@@ -324,5 +324,5 @@ let uninterp_bigQ rc =
let _ = Notation.declare_numeral_interpreter bigQ_scope
(bigQ_path, bigQ_module)
interp_bigQ
- ([RRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
+ ([GRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 7f093ae95..fc953e5e5 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -46,24 +46,24 @@ let four = mult_2 two
(* Unary representation of strictly positive numbers *)
let rec small_r dloc n =
- if equal one n then RRef (dloc, glob_R1)
- else RApp(dloc,RRef (dloc,glob_Rplus),
- [RRef (dloc, glob_R1);small_r dloc (sub_1 n)])
+ if equal one n then GRef (dloc, glob_R1)
+ else GApp(dloc,GRef (dloc,glob_Rplus),
+ [GRef (dloc, glob_R1);small_r dloc (sub_1 n)])
let r_of_posint dloc n =
- let r1 = RRef (dloc, glob_R1) in
+ let r1 = GRef (dloc, glob_R1) in
let r2 = small_r dloc two in
let rec r_of_pos n =
if less_than n four then small_r dloc n
else
let (q,r) = div2_with_rest n in
- let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
- if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in
- if n <> zero then r_of_pos n else RRef(dloc,glob_R0)
+ 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)
let r_of_int dloc z =
if is_strictly_neg z then
- RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
+ GApp (dloc, GRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
else
r_of_posint dloc z
@@ -75,33 +75,33 @@ let bignat_of_r =
(* for numbers > 1 *)
let rec bignat_of_pos = function
(* 1+1 *)
- | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)])
+ | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)])
when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two
(* 1+(1+1) *)
- | RApp (_,RRef (_,p1), [RRef (_,o1);
- RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])])
+ | 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
(* (1+1)*b *)
- | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult ->
+ | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult ->
if bignat_of_pos a <> two then raise Non_closed_number;
mult_2 (bignat_of_pos b)
(* 1+(1+1)*b *)
- | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;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;
add_1 (mult_2 (bignat_of_pos b))
| _ -> raise Non_closed_number
in
let bignat_of_r = function
- | RRef (_,a) when a = glob_R0 -> zero
- | RRef (_,a) when a = glob_R1 -> one
+ | GRef (_,a) when a = glob_R0 -> zero
+ | GRef (_,a) when a = glob_R1 -> one
| r -> bignat_of_pos r
in
bignat_of_r
let bigint_of_r = function
- | RApp (_,RRef (_,o), [a]) when o = glob_Ropp ->
+ | GApp (_,GRef (_,o), [a]) when o = glob_Ropp ->
let n = bignat_of_r a in
if n = zero then raise Non_closed_number;
neg n
@@ -116,8 +116,8 @@ let uninterp_r p =
let _ = Notation.declare_numeral_interpreter "R_scope"
(r_path,["Coq";"Reals";"Rdefinitions"])
r_of_int
- ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
- RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);
- RRef(dummy_loc,glob_R1)],
+ ([GRef(dummy_loc,glob_Ropp);GRef(dummy_loc,glob_R0);
+ GRef(dummy_loc,glob_Rplus);GRef(dummy_loc,glob_Rmult);
+ GRef(dummy_loc,glob_R1)],
uninterp_r,
false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index cb2b16858..61643881e 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -37,8 +37,8 @@ open Lazy
let interp_string dloc s =
let le = String.length s in
let rec aux n =
- if n = le then RRef (dloc, force glob_EmptyString) else
- RApp (dloc,RRef (dloc, force glob_String),
+ if n = le then GRef (dloc, force glob_EmptyString) else
+ GApp (dloc,GRef (dloc, force glob_String),
[interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
in aux 0
@@ -46,11 +46,11 @@ let uninterp_string r =
try
let b = Buffer.create 16 in
let rec aux = function
- | RApp (_,RRef (_,k),[a;s]) when k = force glob_String ->
+ | GApp (_,GRef (_,k),[a;s]) when k = force glob_String ->
(match uninterp_ascii a with
| Some c -> Buffer.add_char b (Char.chr c); aux s
| _ -> raise Non_closed_string)
- | RRef (_,z) when z = force glob_EmptyString ->
+ | GRef (_,z) when z = force glob_EmptyString ->
Some (Buffer.contents b)
| _ ->
raise Non_closed_string
@@ -62,6 +62,6 @@ let _ =
Notation.declare_string_interpreter "string_scope"
(string_path,["Coq";"Strings";"String"])
interp_string
- ([RRef (dummy_loc,static_glob_String);
- RRef (dummy_loc,static_glob_EmptyString)],
+ ([GRef (dummy_loc,static_glob_String);
+ GRef (dummy_loc,static_glob_EmptyString)],
uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index fb8de1f92..81588bced 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -42,13 +42,13 @@ let glob_xO = ConstructRef path_of_xO
let glob_xH = ConstructRef path_of_xH
let pos_of_bignat dloc x =
- let ref_xI = RRef (dloc, glob_xI) in
- let ref_xH = RRef (dloc, glob_xH) in
- let ref_xO = RRef (dloc, glob_xO) in
+ let ref_xI = GRef (dloc, glob_xI) in
+ let ref_xH = GRef (dloc, glob_xH) in
+ let ref_xO = GRef (dloc, glob_xO) in
let rec pos_of x =
match div2_with_rest x with
- | (q,false) -> RApp (dloc, ref_xO,[pos_of q])
- | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q])
+ | (q,false) -> GApp (dloc, ref_xO,[pos_of q])
+ | (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q])
| (q,true) -> ref_xH
in
pos_of x
@@ -66,9 +66,9 @@ let interp_positive dloc n =
(**********************************************************************)
let rec bignat_of_pos = function
- | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
- | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
- | RRef (_, a) when a = glob_xH -> Bigint.one
+ | GApp (_, GRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
+ | GApp (_, GRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
+ | GRef (_, a) when a = glob_xH -> Bigint.one
| _ -> raise Non_closed_number
let uninterp_positive p =
@@ -84,9 +84,9 @@ let uninterp_positive p =
let _ = Notation.declare_numeral_interpreter "positive_scope"
(positive_path,positive_module)
interp_positive
- ([RRef (dummy_loc, glob_xI);
- RRef (dummy_loc, glob_xO);
- RRef (dummy_loc, glob_xH)],
+ ([GRef (dummy_loc, glob_xI);
+ GRef (dummy_loc, glob_xO);
+ GRef (dummy_loc, glob_xH)],
uninterp_positive,
true)
@@ -106,9 +106,9 @@ let n_path = make_path binnat_module "N"
let n_of_binnat dloc pos_or_neg n =
if n <> zero then
- RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n])
+ GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n])
else
- RRef (dloc, glob_N0)
+ GRef (dloc, glob_N0)
let error_negative dloc =
user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
@@ -122,8 +122,8 @@ let n_of_int dloc n =
(**********************************************************************)
let bignat_of_n = function
- | RApp (_, RRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
- | RRef (_, a) when a = glob_N0 -> Bigint.zero
+ | GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
+ | GRef (_, a) when a = glob_N0 -> Bigint.zero
| _ -> raise Non_closed_number
let uninterp_n p =
@@ -136,8 +136,8 @@ let uninterp_n p =
let _ = Notation.declare_numeral_interpreter "N_scope"
(n_path,binnat_module)
n_of_int
- ([RRef (dummy_loc, glob_N0);
- RRef (dummy_loc, glob_Npos)],
+ ([GRef (dummy_loc, glob_N0);
+ GRef (dummy_loc, glob_Npos)],
uninterp_n,
true)
@@ -160,18 +160,18 @@ let z_of_int dloc n =
if n <> zero then
let sgn, n =
if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
- RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
+ GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n])
else
- RRef (dloc, glob_ZERO)
+ GRef (dloc, glob_ZERO)
(**********************************************************************)
(* Printing Z via scopes *)
(**********************************************************************)
let bigint_of_z = function
- | RApp (_, RRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a
- | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a)
- | RRef (_, a) when a = glob_ZERO -> Bigint.zero
+ | GApp (_, GRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a
+ | GApp (_, GRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a)
+ | GRef (_, a) when a = glob_ZERO -> Bigint.zero
| _ -> raise Non_closed_number
let uninterp_z p =
@@ -185,8 +185,8 @@ let uninterp_z p =
let _ = Notation.declare_numeral_interpreter "Z_scope"
(z_path,binint_module)
z_of_int
- ([RRef (dummy_loc, glob_ZERO);
- RRef (dummy_loc, glob_POS);
- RRef (dummy_loc, glob_NEG)],
+ ([GRef (dummy_loc, glob_ZERO);
+ GRef (dummy_loc, glob_POS);
+ GRef (dummy_loc, glob_NEG)],
uninterp_z,
true)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 12:08:42 +0000