Making detyping potentially lazy.

The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.

We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.

Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).

We also fix a regression in the test-suite:

  Mixing laziness and effects is a well-known hell. Here, an exception
  that was raised for mere control purpose was delayed and raised at a
  later time as an anomaly. We make the offending function eager.

6 files changed, 107 insertions, 83 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index c41ec39cb..b299ff853 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -25,6 +25,10 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
 let ascii_module = ["Coq";"Strings";"Ascii"]
 
 let ascii_path = make_path ascii_module "ascii"
@@ -42,9 +46,9 @@ let interp_ascii ?loc p =
   let rec aux n p =
      if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
+     (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
      :: (aux (n-1) (p/2)) in
-  CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
+  DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
 
 let interp_ascii_string ?loc s =
   let p =
@@ -60,12 +64,12 @@ let interp_ascii_string ?loc s =
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
     | [] when Int.equal n 0 -> 0
-    | { 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)
+    | r::l when is_gr r glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
-    let aux = function
-    | { CAst.v = GApp ({ CAst.v = GRef (k,_)},l) } when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
+    let aux c = match DAst.get c with
+    | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
@@ -75,10 +79,10 @@ let make_ascii_string n =
   if n>=32 && n<=126 then String.make 1 (char_of_int n)
   else Printf.sprintf "%03d" n
 
-let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r)
+let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r)
 
 let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
+    ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index af64b1479..0dff047a3 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -23,6 +23,10 @@ open Glob_term
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
 let make_mind mp id = Names.MutInd.make2 mp (Label.make id)
 let make_mind_mpfile dir id = make_mind (ModPath.MPfile (make_dir dir)) id
 let make_mind_mpdot dir modname id =
@@ -49,9 +53,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 = 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 ref_construct = DAst.make ?loc (GRef (int31_construct, None)) in
+  let ref_0 = DAst.make ?loc (GRef (int31_0, None)) in
+  let ref_1 = DAst.make ?loc (GRef (int31_1, None)) in
   let rec args counter n =
     if counter <= 0 then
       []
@@ -59,7 +63,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
-  CAst.make ?loc (GApp (ref_construct, List.rev (args 31 n)))
+  DAst.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.")
@@ -76,15 +80,15 @@ let bigint_of_int31 =
   let rec args_parsing args cur =
     match args with
       | [] -> 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))
+      | r::l when is_gr r int31_0 -> args_parsing l (mult_2 cur)
+      | r::l when is_gr r int31_1 -> args_parsing l (add_1 (mult_2 cur))
       | _ -> raise Non_closed
   in
-  function
-  | { CAst.v = GApp ({ CAst.v = GRef (c, _) }, args) } when eq_gr c int31_construct -> args_parsing args zero
+  fun c -> match DAst.get c with
+  | GApp (r, args) when is_gr r int31_construct -> args_parsing args zero
   | _ -> raise Non_closed
 
-let uninterp_int31 i =
+let uninterp_int31 (AnyGlobConstr i) =
   try
     Some (bigint_of_int31 i)
   with Non_closed ->
@@ -94,6 +98,6 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([CAst.make (GRef (int31_construct, None))],
+  ([DAst.make (GRef (int31_construct, None))],
    uninterp_int31,
    true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 524a5c522..2f9870cf9 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -37,11 +37,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 = CAst.make ?loc @@ GRef (glob_O, None) in
-      let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in
+      let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in
+      let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in
       let rec mk_nat acc n =
 	if n <> zero then
-	  mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
+	  mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
 	else
 	  acc
       in
@@ -56,13 +56,17 @@ let nat_of_int ?loc n =
 
 exception Non_closed_number
 
-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)
+let rec int_of_nat x = DAst.with_val (function
+  | GApp (r, [a]) ->
+    begin match DAst.get r with
+    | GRef (s,_) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
+    | _ -> raise Non_closed_number
+    end
   | GRef (z,_) when Globnames.eq_gr z glob_O -> zero
   | _ -> raise Non_closed_number
   ) x
 
-let uninterp_nat p =
+let uninterp_nat (AnyGlobConstr p) =
   try
     Some (int_of_nat p)
   with
@@ -75,4 +79,4 @@ let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (nat_path,datatypes_module_name)
     nat_of_int
-    ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true)
+    ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 06117de79..88ff38c6d 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -27,6 +27,10 @@ let binnums = ["Coq";"Numbers";"BinNums"]
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
 let positive_path = make_path binnums "positive"
 
 (* TODO: temporary hack *)
@@ -42,13 +46,13 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat ?loc x =
-  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 ref_xI = DAst.make @@ GRef (glob_xI, None) in
+  let ref_xH = DAst.make @@ GRef (glob_xH, None) in
+  let ref_xO = DAst.make @@ GRef (glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
-      | (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,false) -> DAst.make @@ GApp (ref_xO,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -57,10 +61,10 @@ let pos_of_bignat ?loc x =
 (* Printing positive via scopes                                       *)
 (**********************************************************************)
 
-let rec bignat_of_pos = function
-  | { 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
+let rec bignat_of_pos c = match DAst.get c with
+  | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
+  | GApp (r, [a]) when is_gr r 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
 
 (**********************************************************************)
@@ -81,18 +85,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
-    CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
+    DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
   else
-    CAst.make @@ GRef (glob_ZERO, None)
+    DAst.make @@ GRef (glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
-let bigint_of_z = function
-  | { 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
+let bigint_of_z c = match DAst.get c with
+  | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a
+  | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -108,18 +112,18 @@ 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 =
-  CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
+  DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
 (**********************************************************************)
 
-let bigint_of_r = function
-  | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR ->
+let bigint_of_r c = match DAst.get c with
+  | GApp (r, [a]) when is_gr r glob_IZR ->
       bigint_of_z a
   | _ -> raise Non_closed_number
 
-let uninterp_r p =
+let uninterp_r (AnyGlobConstr p) =
   try
     Some (bigint_of_r p)
   with Non_closed_number ->
@@ -128,6 +132,6 @@ let uninterp_r p =
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (r_path,["Coq";"Reals";"Rdefinitions"])
   r_of_int
-  ([CAst.make @@ GRef (glob_IZR, None)],
+  ([DAst.make @@ GRef (glob_IZR, None)],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index b7f13b040..cc82fc94c 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -31,25 +31,29 @@ let make_reference id = find_reference "String interpretation" string_module id
 let glob_String = lazy (make_reference "String")
 let glob_EmptyString = lazy (make_reference "EmptyString")
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
 open Lazy
 
 let interp_string ?loc s =
   let le = String.length s in
   let rec aux n =
-     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),
+     if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else
+     DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None),
        [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
-let uninterp_string r =
+let uninterp_string (AnyGlobConstr r) =
   try
     let b = Buffer.create 16 in
-    let rec aux = function
-    | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_gr k (force glob_String) ->
+    let rec aux c = match DAst.get c with
+    | GApp (k,[a;s]) when is_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)
-    | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) ->
+    | GRef (z,_) when eq_gr z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -61,6 +65,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([CAst.make @@ GRef (static_glob_String,None);
-      CAst.make @@ GRef (static_glob_EmptyString,None)],
+    ([DAst.make @@ GRef (static_glob_String,None);
+      DAst.make @@ GRef (static_glob_EmptyString,None)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index af3df2889..0d743a2b5 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 = 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 ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in
+  let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in
+  let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
-      | (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,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -68,14 +68,18 @@ let interp_positive ?loc n =
 (* Printing positive via scopes                                       *)
 (**********************************************************************)
 
-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))
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
+let rec bignat_of_pos x = DAst.with_val (function
+  | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
+  | GApp (r ,[a]) when is_gr r 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 =
+let uninterp_positive (AnyGlobConstr p) =
   try
     Some (bignat_of_pos p)
   with Non_closed_number ->
@@ -88,9 +92,9 @@ let uninterp_positive p =
 let _ = Notation.declare_numeral_interpreter "positive_scope"
   (positive_path,binnums)
   interp_positive
-  ([CAst.make @@ GRef (glob_xI, None);
-    CAst.make @@ GRef (glob_xO, None);
-    CAst.make @@ GRef (glob_xH, None)],
+  ([DAst.make @@ GRef (glob_xI, None);
+    DAst.make @@ GRef (glob_xO, None);
+    DAst.make @@ GRef (glob_xH, None)],
    uninterp_positive,
    true)
 
@@ -107,9 +111,9 @@ let glob_Npos = ConstructRef path_of_Npos
 
 let n_path = make_path binnums "N"
 
-let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@
+let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@
   if not (Bigint.equal n zero) then
-    GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
+    GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
   else
     GRef(glob_N0, None)
 
@@ -124,13 +128,13 @@ let n_of_int ?loc n =
 (* Printing N via scopes                                              *)
 (**********************************************************************)
 
-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
+let bignat_of_n n = DAst.with_val (function
+  | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a
   | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
-  )
+  ) n
 
-let uninterp_n p =
+let uninterp_n (AnyGlobConstr p) =
   try Some (bignat_of_n p)
   with Non_closed_number -> None
 
@@ -140,8 +144,8 @@ let uninterp_n p =
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (n_path,binnums)
   n_of_int
-  ([CAst.make @@ GRef (glob_N0, None);
-    CAst.make @@ GRef (glob_Npos, None)],
+  ([DAst.make @@ GRef (glob_N0, None);
+    DAst.make @@ GRef (glob_Npos, None)],
   uninterp_n,
   true)
 
@@ -163,22 +167,22 @@ 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
-    CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
+    DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
   else
-    CAst.make ?loc @@ GRef(glob_ZERO, None)
+    DAst.make ?loc @@ GRef(glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
-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)
+let bigint_of_z z = DAst.with_val (function
+  | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a
+  | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
   | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
-  )
+  ) z
 
-let uninterp_z p =
+let uninterp_z (AnyGlobConstr p) =
   try
     Some (bigint_of_z p)
   with Non_closed_number -> None
@@ -189,8 +193,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([CAst.make @@ GRef (glob_ZERO, None);
-    CAst.make @@ GRef (glob_POS, None);
-    CAst.make @@ GRef (glob_NEG, None)],
+  ([DAst.make @@ GRef (glob_ZERO, None);
+    DAst.make @@ GRef (glob_POS, None);
+    DAst.make @@ GRef (glob_NEG, None)],
   uninterp_z,
   true)