[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

2 files changed, 13 insertions, 13 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 33e7236f5..e6c82c894 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -226,19 +226,19 @@ GEXTEND Gram
 
   record_field_declaration:
     [ [ id = global; bl = binders; ":="; c = lconstr ->
-      (id, mkCLambdaN (!@loc) bl c) ] ]
+      (id, mkCLambdaN ~loc:!@loc bl c) ] ]
   ;
   binder_constr:
     [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
-          mkCProdN (!@loc) bl c
+          mkCProdN ~loc:!@loc bl c
       | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
-          mkCLambdaN (!@loc) bl c
+          mkCLambdaN ~loc:!@loc bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
           let ty,c1 = match ty, c1 with
           | (_,None), (_, CCast(c, CastConv t)) -> (Loc.tag ~loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
           | _, _ -> ty, c1 in
-          Loc.tag ~loc:!@loc @@ CLetIn(id,mkCLambdaN (constr_loc c1) bl c1,
+          Loc.tag ~loc:!@loc @@ CLetIn(id,mkCLambdaN ~loc:(constr_loc c1) bl c1,
                  Option.map (mkCProdN ~loc:(fst ty) bl) (snd ty), c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
@@ -411,7 +411,7 @@ GEXTEND Gram
         (fun na -> CLocalAssum (na::nal,Default Implicit,c))
     | nal=LIST1 name; "}" ->
         (fun na -> CLocalAssum (na::nal,Default Implicit,
-                                Loc.tag ~loc:(Loc.join_loc (fst na) !@loc) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
+                                Loc.tag ~loc:(Loc.merge (fst na) !@loc) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
     | ":"; c=lconstr; "}" ->
 	(fun na -> CLocalAssum ([na],Default Implicit,c))
     ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3d0322b10..7a3a2ace1 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -349,14 +349,14 @@ GEXTEND Gram
   ;
   record_binder_body:
     [ [ l = binders; oc = of_type_with_opt_coercion;
-         t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t))
+         t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN ~loc:!@loc l t))
       | l = binders; oc = of_type_with_opt_coercion;
          t = lconstr; ":="; b = lconstr -> fun id ->
-	   (oc,DefExpr (id,mkCLambdaN ~loc:!@loc l b,Some (mkCProdN (!@loc) l t)))
+	   (oc,DefExpr (id,mkCLambdaN ~loc:!@loc l b,Some (mkCProdN ~loc:!@loc l t)))
       | l = binders; ":="; b = lconstr -> fun id ->
          match snd b with
 	 | CCast(b', (CastConv t|CastVM t|CastNative t)) ->
-	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b',Some (mkCProdN (!@loc) l t)))
+	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b',Some (mkCProdN ~loc:!@loc l t)))
          | _ ->
 	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ]
   ;
@@ -378,9 +378,9 @@ GEXTEND Gram
   constructor_type:
     [[ l = binders;
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
-	            fun l id -> (not (Option.is_empty coe),(id,mkCProdN (!@loc) l c))
+	            fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c))
             |  ->
-		 fun l id -> (false,(id,mkCProdN (!@loc) l (Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ]
+		 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ]
 	 -> t l
      ]]
 ;
@@ -592,15 +592,15 @@ GEXTEND Gram
           d = def_body ->
           let s = coerce_reference_to_id qid in
 	  VernacDefinition
-	    ((Some Global,CanonicalStructure),((Loc.ghost,s),None),d)
+	    ((Some Global,CanonicalStructure),((Loc.tag s),None),d)
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-	  VernacDefinition ((None,Coercion),((Loc.ghost,s),None),d)
+	  VernacDefinition ((None,Coercion),((Loc.tag s),None),d)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = coerce_reference_to_id qid in
-	  VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.ghost,s),None),d)
+	  VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.tag s),None),d)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
 	   VernacIdentityCoercion (true, f, s, t)