[location] [ast] Port module AST to CAst

6 files changed, 97 insertions, 94 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index ed977c416..e7eea0284 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -41,9 +41,9 @@ let interp_ascii ?loc p =
   let rec aux n p =
      if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     (Loc.tag ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
+     (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
      :: (aux (n-1) (p/2)) in
-  Loc.tag ?loc @@ GApp (Loc.tag ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
+  CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
 
 let interp_ascii_string ?loc s =
   let p =
@@ -59,12 +59,12 @@ let interp_ascii_string ?loc s =
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
     | [] 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)
+    | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | { CAst.v = 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 Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
+    | { CAst.v = GApp ({ CAst.v = 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
@@ -80,4 +80,4 @@ let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([Loc.tag @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
+    ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 5cdd82024..9a4cd6c25 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -36,11 +36,11 @@ let warn_large_nat =
 let nat_of_int ?loc n =
   if is_pos_or_zero n then begin
       if less_than threshold n then warn_large_nat ();
-      let ref_O = Loc.tag ?loc @@ GRef (glob_O, None) in
-      let ref_S = Loc.tag ?loc @@ GRef (glob_S, None) in
+      let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in
+      let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in
       let rec mk_nat acc n =
 	if n <> zero then
-	  mk_nat (Loc.tag ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
+	  mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
 	else
 	  acc
       in
@@ -55,8 +55,8 @@ let nat_of_int ?loc n =
 
 exception Non_closed_number
 
-let rec int_of_nat x = Loc.with_unloc (function
-  | GApp ((_, GRef (s,_)),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
+let rec int_of_nat x = CAst.with_val (function
+  | GApp ({ CAst.v = 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
   ) x
@@ -74,4 +74,4 @@ let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (nat_path,datatypes_module_name)
     nat_of_int
-    ([Loc.tag @@ GRef (glob_S,None); Loc.tag @@ GRef (glob_O,None)], uninterp_nat, true)
+    ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 3ee64ba7e..e23852bf8 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -87,9 +87,9 @@ exception Non_closed
 (* parses a *non-negative* integer (from bigint.ml) into an int31
    wraps modulo 2^31 *)
 let int31_of_pos_bigint ?loc n =
-  let ref_construct = Loc.tag ?loc @@ GRef (int31_construct, None) in
-  let ref_0 = Loc.tag ?loc @@ GRef (int31_0, None) in
-  let ref_1 = Loc.tag ?loc @@ GRef (int31_1, None) in
+  let ref_construct = CAst.make ?loc @@ GRef (int31_construct, None) in
+  let ref_0 = CAst.make ?loc @@ GRef (int31_0, None) in
+  let ref_1 = CAst.make ?loc @@ GRef (int31_1, None) in
   let rec args counter n =
     if counter <= 0 then
       []
@@ -97,7 +97,7 @@ let int31_of_pos_bigint ?loc n =
       let (q,r) = div2_with_rest n in
 	(if r then ref_1 else ref_0)::(args (counter-1) q)
   in
-  Loc.tag ?loc @@ GApp (ref_construct, List.rev (args 31 n))
+  CAst.make ?loc @@ GApp (ref_construct, List.rev (args 31 n))
 
 let error_negative ?loc =
   CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
@@ -114,12 +114,12 @@ let bigint_of_int31 =
   let rec args_parsing args cur =
     match args with
       | [] -> 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))
+      | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
+      | { CAst.v = 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 eq_gr c int31_construct -> args_parsing args zero
+  | { CAst.v = GApp ({ CAst.v = GRef (c, _)}, args) } when eq_gr c int31_construct -> args_parsing args zero
   | _ -> raise Non_closed
 
 let uninterp_int31 i =
@@ -132,7 +132,7 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([Loc.tag @@ GRef (int31_construct, None)],
+  ([CAst.make @@ GRef (int31_construct, None)],
    uninterp_int31,
    true)
 
@@ -163,16 +163,16 @@ let height bi =
 
 (* n must be a non-negative integer (from bigint.ml) *)
 let word_of_pos_bigint ?loc hght n =
-  let ref_W0 = Loc.tag ?loc @@ GRef (zn2z_W0, None) in
-  let ref_WW = Loc.tag ?loc @@ GRef (zn2z_WW, None) in
+  let ref_W0 = CAst.make ?loc @@ GRef (zn2z_W0, None) in
+  let ref_WW = CAst.make ?loc @@ GRef (zn2z_WW, None) in
   let rec decomp hgt n =
     if hgt <= 0 then
       int31_of_pos_bigint ?loc n
     else if equal n zero then
-      Loc.tag ?loc @@ GApp (ref_W0, [Loc.tag ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
+      CAst.make ?loc @@ GApp (ref_W0, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
     else
       let (h,l) = split_at hgt n in
-      Loc.tag ?loc @@ GApp (ref_WW, [Loc.tag ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
+      CAst.make ?loc @@ GApp (ref_WW, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
 			   decomp (hgt-1) h;
 			   decomp (hgt-1) l])
   in
@@ -180,13 +180,13 @@ let word_of_pos_bigint ?loc hght n =
 
 let bigN_of_pos_bigint ?loc n =
   let h = height n in
-  let ref_constructor = Loc.tag ?loc @@ GRef (bigN_constructor h, None) in
+  let ref_constructor = CAst.make ?loc @@ GRef (bigN_constructor h, None) in
   let word = word_of_pos_bigint ?loc h n in
   let args =
     if h < n_inlined then [word]
     else [Nat_syntax_plugin.Nat_syntax.nat_of_int ?loc (of_int (h-n_inlined));word]
   in
-  Loc.tag ?loc @@ GApp (ref_constructor, args)
+  CAst.make ?loc @@ GApp (ref_constructor, args)
 
 let bigN_error_negative ?loc =
   CErrors.user_err ?loc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.")
@@ -203,14 +203,14 @@ let interp_bigN ?loc n =
 let bigint_of_word =
   let rec get_height rc =
     match rc with
-    | _, GApp ((_, GRef(c,_)), [_;lft;rght]) when eq_gr c zn2z_WW ->
+    | { CAst.v = GApp ({ CAst.v = 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 eq_gr c zn2z_W0-> zero
-    | _, GApp ((_, GRef(c,_)), [_;lft;rght]) when eq_gr c zn2z_WW->
+    | { CAst.v = GApp ({ CAst.v = GRef(c,_)},_)} when eq_gr c zn2z_W0-> zero
+    | { CAst.v = GApp ({ CAst.v = 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))
@@ -223,8 +223,8 @@ let bigint_of_word =
 
 let bigint_of_bigN rc =
   match rc with
-  | _, GApp (_,[one_arg]) -> bigint_of_word one_arg
-  | _, GApp (_,[_;second_arg]) -> bigint_of_word second_arg
+  | { CAst.v = GApp (_,[one_arg]) } -> bigint_of_word one_arg
+  | { CAst.v = GApp (_,[_;second_arg]) } -> bigint_of_word second_arg
   | _ -> raise Non_closed
 
 let uninterp_bigN rc =
@@ -240,7 +240,7 @@ let uninterp_bigN rc =
 let bigN_list_of_constructors =
   let rec build i =
     if i < n_inlined+1 then
-      (Loc.tag @@ GRef (bigN_constructor i,None))::(build (i+1))
+      (CAst.make @@ GRef (bigN_constructor i,None))::(build (i+1))
     else
       []
   in
@@ -257,17 +257,17 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
 
 (*** Parsing for bigZ in digital notation ***)
 let interp_bigZ ?loc n =
-  let ref_pos = Loc.tag ?loc @@ GRef (bigZ_pos, None) in
-  let ref_neg = Loc.tag ?loc @@ GRef (bigZ_neg, None) in
+  let ref_pos = CAst.make ?loc @@ GRef (bigZ_pos, None) in
+  let ref_neg = CAst.make ?loc @@ GRef (bigZ_neg, None) in
   if is_pos_or_zero n then
-    Loc.tag ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n])
+    CAst.make ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n])
   else
-    Loc.tag ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)])
+    CAst.make ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)])
 
 (* pretty printing functions for bigZ *)
 let bigint_of_bigZ = function
-  | _, 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 ->
+  | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
+  | { CAst.v = GApp ({ CAst.v = 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
@@ -286,19 +286,19 @@ let uninterp_bigZ rc =
 let _ = Notation.declare_numeral_interpreter bigZ_scope
   (bigZ_path, bigZ_module)
   interp_bigZ
-  ([Loc.tag @@ GRef (bigZ_pos, None);
-    Loc.tag @@ GRef (bigZ_neg, None)],
+  ([CAst.make @@ GRef (bigZ_pos, None);
+    CAst.make @@ GRef (bigZ_neg, None)],
    uninterp_bigZ,
    true)
 
 (*** Parsing for bigQ in digital notation ***)
 let interp_bigQ ?loc n =
-  let ref_z = Loc.tag ?loc @@ GRef (bigQ_z, None) in
-  Loc.tag ?loc @@ GApp (ref_z, [interp_bigZ ?loc n])
+  let ref_z = CAst.make ?loc @@ GRef (bigQ_z, None) in
+  CAst.make ?loc @@ GApp (ref_z, [interp_bigZ ?loc n])
 
 let uninterp_bigQ rc =
   try match rc with
-    | _, GApp ((_, GRef(c,_)), [one_arg]) when eq_gr c bigQ_z ->
+    | { CAst.v = GApp ({ CAst.v = 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
@@ -307,5 +307,5 @@ let uninterp_bigQ rc =
 let _ = Notation.declare_numeral_interpreter bigQ_scope
   (bigQ_path, bigQ_module)
   interp_bigQ
-  ([Loc.tag @@ GRef (bigQ_z, None)], uninterp_bigQ,
+  ([CAst.make @@ GRef (bigQ_z, None)], uninterp_bigQ,
    true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index b7041d045..7ce066c59 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -42,13 +42,13 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat ?loc x =
-  let ref_xI = Loc.tag @@ GRef (glob_xI, None) in
-  let ref_xH = Loc.tag @@ GRef (glob_xH, None) in
-  let ref_xO = Loc.tag @@ GRef (glob_xO, None) in
+  let ref_xI = CAst.make @@ GRef (glob_xI, None) in
+  let ref_xH = CAst.make @@ GRef (glob_xH, None) in
+  let ref_xO = CAst.make @@ GRef (glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
-      | (q,false) -> Loc.tag @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> Loc.tag @@ GApp (ref_xI,[pos_of q])
+      | (q,false) -> CAst.make @@ GApp (ref_xO,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -58,9 +58,9 @@ let pos_of_bignat ?loc x =
 (**********************************************************************)
 
 let rec bignat_of_pos = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | _, GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
+  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -81,18 +81,18 @@ let z_of_int ?loc n =
   if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    Loc.tag @@ GApp(Loc.tag @@ GRef (sgn,None), [pos_of_bignat ?loc n])
+    CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
   else
-    Loc.tag @@ GRef (glob_ZERO, None)
+    CAst.make @@ GRef (glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
 let bigint_of_z = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | _, GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -108,14 +108,14 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id)
 let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR")
 
 let r_of_int ?loc z =
-  Loc.tag @@ GApp (Loc.tag @@ GRef(glob_IZR,None), [z_of_int ?loc z])
+  CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
 (**********************************************************************)
 
 let bigint_of_r = function
-  | _, GApp ((_, GRef (o,_)), [a]) when Globnames.eq_gr o glob_IZR ->
+  | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR ->
       bigint_of_z a
   | _ -> raise Non_closed_number
 
@@ -128,6 +128,6 @@ let uninterp_r p =
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (r_path,["Coq";"Reals";"Rdefinitions"])
   r_of_int
-  ([Loc.tag @@ GRef (glob_IZR, None)],
+  ([CAst.make @@ GRef (glob_IZR, None)],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 49cb9355c..b7f13b040 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -36,8 +36,8 @@ open Lazy
 let interp_string ?loc s =
   let le = String.length s in
   let rec aux n =
-     if n = le then Loc.tag ?loc @@ GRef (force glob_EmptyString, None) else
-     Loc.tag ?loc @@ GApp (Loc.tag ?loc @@ GRef (force glob_String, None),
+     if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else
+     CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None),
        [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
@@ -45,11 +45,11 @@ let uninterp_string r =
   try
     let b = Buffer.create 16 in
     let rec aux = function
-    | _, GApp ((_, GRef (k,_)),[a;s]) when eq_gr k (force glob_String) ->
+    | { CAst.v = GApp ({ CAst.v = 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 eq_gr z (force glob_EmptyString) ->
+    | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -61,6 +61,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([Loc.tag @@ GRef (static_glob_String,None);
-      Loc.tag @@ GRef (static_glob_EmptyString,None)],
+    ([CAst.make @@ GRef (static_glob_String,None);
+      CAst.make @@ GRef (static_glob_EmptyString,None)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 96c1f3e39..479448e06 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -45,13 +45,13 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat ?loc x = 
-  let ref_xI = Loc.tag ?loc @@ GRef (glob_xI, None) in
-  let ref_xH = Loc.tag ?loc @@ GRef (glob_xH, None) in
-  let ref_xO = Loc.tag ?loc @@ GRef (glob_xO, None) in
+  let ref_xI = CAst.make ?loc @@ GRef (glob_xI, None) in
+  let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in
+  let ref_xO = CAst.make ?loc @@ GRef (glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
-      | (q,false) -> Loc.tag ?loc @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> Loc.tag ?loc @@ GApp (ref_xI,[pos_of q])
+      | (q,false) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> CAst.make ?loc @@ GApp (ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -68,11 +68,12 @@ let interp_positive ?loc n =
 (* Printing positive via scopes                                       *)
 (**********************************************************************)
 
-let rec bignat_of_pos = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | _, GRef (a, _)                when Globnames.eq_gr a glob_xH -> Bigint.one
+let rec bignat_of_pos x = CAst.with_val (function
+  | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+  | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | GRef (a, _)                when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
+  ) x
 
 let uninterp_positive p =
   try
@@ -87,9 +88,9 @@ let uninterp_positive p =
 let _ = Notation.declare_numeral_interpreter "positive_scope"
   (positive_path,binnums)
   interp_positive
-  ([Loc.tag @@ GRef (glob_xI, None);
-    Loc.tag @@ GRef (glob_xO, None);
-    Loc.tag @@ GRef (glob_xH, None)],
+  ([CAst.make @@ GRef (glob_xI, None);
+    CAst.make @@ GRef (glob_xO, None);
+    CAst.make @@ GRef (glob_xH, None)],
    uninterp_positive,
    true)
 
@@ -106,9 +107,9 @@ let glob_Npos = ConstructRef path_of_Npos
 
 let n_path = make_path binnums "N"
 
-let n_of_binnat ?loc pos_or_neg n = Loc.tag ?loc @@
+let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@
   if not (Bigint.equal n zero) then
-    GApp(Loc.tag @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
+    GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
   else
     GRef(glob_N0, None)
 
@@ -123,10 +124,11 @@ let n_of_int ?loc n =
 (* Printing N via scopes                                              *)
 (**********************************************************************)
 
-let bignat_of_n = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
-  | _, GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
+let bignat_of_n = CAst.with_val (function
+  | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
+  | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
+  )
 
 let uninterp_n p =
   try Some (bignat_of_n p)
@@ -138,8 +140,8 @@ let uninterp_n p =
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (n_path,binnums)
   n_of_int
-  ([Loc.tag @@ GRef (glob_N0, None);
-    Loc.tag @@ GRef (glob_Npos, None)],
+  ([CAst.make @@ GRef (glob_N0, None);
+    CAst.make @@ GRef (glob_Npos, None)],
   uninterp_n,
   true)
 
@@ -161,19 +163,20 @@ let z_of_int ?loc n =
   if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    Loc.tag ?loc @@ GApp(Loc.tag ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
+    CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
   else
-    Loc.tag ?loc @@ GRef(glob_ZERO, None)
+    CAst.make ?loc @@ GRef(glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
-let bigint_of_z = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | _, GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+let bigint_of_z = CAst.with_val (function
+  | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+  | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
+  )
 
 let uninterp_z p =
   try
@@ -186,8 +189,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([Loc.tag @@ GRef (glob_ZERO, None);
-    Loc.tag @@ GRef (glob_POS, None);
-    Loc.tag @@ GRef (glob_NEG, None)],
+  ([CAst.make @@ GRef (glob_ZERO, None);
+    CAst.make @@ GRef (glob_POS, None);
+    CAst.make @@ GRef (glob_NEG, None)],
   uninterp_z,
   true)