[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

6 files changed, 76 insertions, 76 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index dc0b87793..ed977c416 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -37,24 +37,24 @@ let glob_Ascii = lazy (make_reference "Ascii")
 
 open Lazy
 
-let interp_ascii loc p =
+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))
+     (Loc.tag ?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)
+  Loc.tag ?loc @@ GApp (Loc.tag ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
 
-let interp_ascii_string dloc s =
+let interp_ascii_string ?loc s =
   let p =
     if Int.equal (String.length s) 1 then int_of_char s.[0]
     else
       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 ~hdr:"interp_ascii_string"
+	user_err ?loc ~hdr:"interp_ascii_string"
 	 (str "Expects a single character or a three-digits ascii code.") in
-  interp_ascii dloc p
+  interp_ascii ?loc p
 
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 90d643b7f..5cdd82024 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -33,21 +33,21 @@ let warn_large_nat =
                  strbrk "may vary from 5000 to 70000 depending on your system " ++
                  strbrk "limits and on the command executed).")
 
-let nat_of_int loc n =
+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 = Loc.tag ?loc @@ GRef (glob_O, None) in
+      let ref_S = Loc.tag ?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 (Loc.tag ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
 	else
 	  acc
       in
       mk_nat ref_O n
     end
   else
-      user_err ~hdr:"nat_of_int"
+      user_err ?loc ~hdr:"nat_of_int"
        (str "Cannot interpret a negative number as a number of type nat")
 
 (************************************************************************)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 8876d464a..3ee64ba7e 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -86,10 +86,10 @@ 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 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 rec args counter n =
     if counter <= 0 then
       []
@@ -97,16 +97,16 @@ 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))
+  Loc.tag ?loc @@ GApp (ref_construct, List.rev (args 31 n))
 
-let error_negative dloc =
-  CErrors.user_err ~loc:dloc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
+let error_negative ?loc =
+  CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
 
-let interp_int31 dloc n =
+let interp_int31 ?loc n =
   if is_pos_or_zero n then
-    int31_of_pos_bigint dloc n
+    int31_of_pos_bigint ?loc n
   else
-    error_negative dloc
+    error_negative ?loc
 
 (* Pretty prints an int31 *)
 
@@ -162,40 +162,40 @@ let height bi =
   in hght 0 base
 
 (* 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 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 rec decomp hgt n =
     if hgt <= 0 then
-      int31_of_pos_bigint loc n
+      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)])
+      Loc.tag ?loc @@ GApp (ref_W0, [Loc.tag ?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);
+      Loc.tag ?loc @@ GApp (ref_WW, [Loc.tag ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
 			   decomp (hgt-1) h;
 			   decomp (hgt-1) l])
   in
   decomp hght n
 
-let bigN_of_pos_bigint loc 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 word = word_of_pos_bigint loc h n in
+  let ref_constructor = Loc.tag ?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]
+    else [Nat_syntax_plugin.Nat_syntax.nat_of_int ?loc (of_int (h-n_inlined));word]
   in
-  Loc.tag ~loc @@ GApp (ref_constructor, args)
+  Loc.tag ?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.")
+let bigN_error_negative ?loc =
+  CErrors.user_err ?loc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.")
 
-let interp_bigN dloc n =
+let interp_bigN ?loc n =
   if is_pos_or_zero n then
-    bigN_of_pos_bigint dloc n
+    bigN_of_pos_bigint ?loc n
   else
-    bigN_error_negative dloc
+    bigN_error_negative ?loc
 
 
 (* Pretty prints a bigN *)
@@ -256,13 +256,13 @@ 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 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
   if is_pos_or_zero n then
-    Loc.tag ~loc @@ GApp (ref_pos, [bigN_of_pos_bigint loc n])
+    Loc.tag ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n])
   else
-    Loc.tag ~loc @@ GApp (ref_neg, [bigN_of_pos_bigint loc (neg n)])
+    Loc.tag ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)])
 
 (* pretty printing functions for bigZ *)
 let bigint_of_bigZ = function
@@ -292,9 +292,9 @@ let _ = Notation.declare_numeral_interpreter bigZ_scope
    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 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 uninterp_bigQ rc =
   try match rc with
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 1af3f6c5b..b7041d045 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -41,7 +41,7 @@ let glob_xI = ConstructRef path_of_xI
 let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
-let pos_of_bignat dloc x =
+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
@@ -77,11 +77,11 @@ let glob_ZERO = ConstructRef path_of_ZERO
 let glob_POS = ConstructRef path_of_POS
 let glob_NEG = ConstructRef path_of_NEG
 
-let z_of_int dloc n =
+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 dloc n])
+    Loc.tag @@ GApp(Loc.tag @@ GRef (sgn,None), [pos_of_bignat ?loc n])
   else
     Loc.tag @@ GRef (glob_ZERO, None)
 
@@ -107,8 +107,8 @@ 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 dloc z =
-  Loc.tag @@ GApp (Loc.tag @@ GRef(glob_IZR,None), [z_of_int dloc z])
+let r_of_int ?loc z =
+  Loc.tag @@ GApp (Loc.tag @@ GRef(glob_IZR,None), [z_of_int ?loc z])
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
@@ -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)],
+  ([Loc.tag @@ GRef (glob_IZR, None)],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 539670722..49cb9355c 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -33,12 +33,12 @@ let glob_EmptyString = lazy (make_reference "EmptyString")
 
 open Lazy
 
-let interp_string loc s =
+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),
-       [interp_ascii loc (int_of_char s.[n]); aux (n+1)])
+     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),
+       [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
 let uninterp_string r =
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index a00525f91..96c1f3e39 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -44,25 +44,25 @@ let glob_xI = ConstructRef path_of_xI
 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 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 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) -> 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,true) -> ref_xH
   in
   pos_of x
 
-let error_non_positive dloc =
-  user_err ~loc:dloc ~hdr:"interp_positive"
+let error_non_positive ?loc =
+  user_err ?loc ~hdr:"interp_positive"
    (str "Only strictly positive numbers in type \"positive\".")
 
-let interp_positive dloc n =
-  if is_strictly_pos n then pos_of_bignat dloc n
-  else error_non_positive dloc
+let interp_positive ?loc n =
+  if is_strictly_pos n then pos_of_bignat ?loc n
+  else error_non_positive ?loc
 
 (**********************************************************************)
 (* Printing positive via scopes                                       *)
@@ -106,18 +106,18 @@ 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 = Loc.tag ?loc @@
   if not (Bigint.equal n zero) then
-    GApp(Loc.tag @@ GRef (glob_Npos,None), [pos_of_bignat loc n])
+    GApp(Loc.tag @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
   else
     GRef(glob_N0, None)
 
-let error_negative dloc =
-  user_err ~loc:dloc ~hdr:"interp_N" (str "No negative numbers in type \"N\".")
+let error_negative ?loc =
+  user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".")
 
-let n_of_int dloc n =
-  if is_pos_or_zero n then n_of_binnat dloc true n
-  else error_negative dloc
+let n_of_int ?loc n =
+  if is_pos_or_zero n then n_of_binnat ?loc true n
+  else error_negative ?loc
 
 (**********************************************************************)
 (* Printing N via scopes                                              *)
@@ -157,13 +157,13 @@ let glob_ZERO = ConstructRef path_of_ZERO
 let glob_POS = ConstructRef path_of_POS
 let glob_NEG = ConstructRef path_of_NEG
 
-let z_of_int loc n =
+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])
+    Loc.tag ?loc @@ GApp(Loc.tag ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
   else
-    Loc.tag ~loc @@ GRef(glob_ZERO, None)
+    Loc.tag ?loc @@ GRef(glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)