[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

6 files changed, 31 insertions, 33 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 07a0d5a505..946ee55d46 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -672,9 +672,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	  in
 	  let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
 	  assert (Int.equal (Array.length case_pats) 1);
-	  let br =
-	    (Loc.ghost,([],[case_pats.(0)],e))
-	  in
+	  let br = Loc.tag ([],[case_pats.(0)],e) in
 	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
 	  build_entry_lc env funnames avoid match_expr
 
@@ -1254,7 +1252,7 @@ let rec rebuild_return_type (loc, rt) =
         Loc.tag ~loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
     | Constrexpr.CLetIn(na,v,t,t') ->
 	Loc.tag ~loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
-    | _ -> Loc.tag ~loc @@ Constrexpr.CProdN([[Loc.ghost,Anonymous],
+    | _ -> Loc.tag ~loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
 				       Constrexpr.Default Decl_kinds.Explicit,Loc.tag ~loc rt],
 			    Loc.tag @@ Constrexpr.CSort(GType []))
 
@@ -1307,12 +1305,12 @@ let do_build_inductive
 	(fun (n,t,typ) acc ->
           match typ with
           | Some typ ->
-	     Loc.tag @@ Constrexpr.CLetIn((Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+	     Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			      acc)
 	  | None ->
 	     Loc.tag @@ Constrexpr.CProdN
-	       ([[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
+	       ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 		acc
 	       )
 	)
@@ -1374,12 +1372,12 @@ let do_build_inductive
       (fun (n,t,typ) acc ->
          match typ with
          | Some typ ->
-	   Loc.tag @@ Constrexpr.CLetIn((Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+	   Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			    acc)
 	 | None ->
            Loc.tag @@ Constrexpr.CProdN
-	   ([[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
+	   ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 	    acc
 	   )
       )
@@ -1406,18 +1404,18 @@ let do_build_inductive
       (fun (n,t,typ) ->
          match typ with
          | Some typ ->
-	   Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t,
+	   Constrexpr.CLocalDef((Loc.tag n), Constrextern.extern_glob_constr Id.Set.empty t,
                                   Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ))
 	 | None ->
 	 Constrexpr.CLocalAssum
-	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
+	   ([(Loc.tag n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
       )
       rels_params
   in
   let ext_rels_constructors =
     Array.map (List.map
       (fun (id,t) ->
-	 false,((Loc.ghost,id),
+	 false,((Loc.tag id),
 		with_full_print
 		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
 	       )
@@ -1425,7 +1423,7 @@ let do_build_inductive
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors =
-    (((Loc.ghost,relnames.(i)), None),
+    (((Loc.tag @@ relnames.(i)), None),
     rel_params,
     Some rel_arities.(i),
     ext_rel_constructors),[]
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index cad96946ca..1da85c467a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -156,7 +156,7 @@ let build_newrecursive
   let (rec_sign,rec_impls) =
     List.fold_left
       (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
-        let arityc = Constrexpr_ops.mkCProdN Loc.ghost bl arityc in
+        let arityc = Constrexpr_ops.mkCProdN bl arityc in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
 	let evdref = ref (Evd.from_env env0) in
 	let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
@@ -355,7 +355,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	(*i The next call to mk_rel_id is valid since we have just construct the graph
 	   Ensures by : do_built
 	i*)
-	let f_R_mut = Ident (Loc.ghost,mk_rel_id (List.nth names 0)) in
+	let f_R_mut = Ident (Loc.tag @@ mk_rel_id (List.nth names 0)) in
 	let ind_kn =
 	  fst (locate_with_msg
 		 (pr_reference f_R_mut++str ": Not an inductive type!")
@@ -453,7 +453,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
 let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook
     =
-  let type_of_f = Constrexpr_ops.mkCProdN Loc.ghost args ret_type in
+  let type_of_f = Constrexpr_ops.mkCProdN args ret_type in
   let rec_arg_num =
     let names =
       List.map
@@ -470,7 +470,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   let unbounded_eq =
     let f_app_args =
       Loc.tag @@ Constrexpr.CAppExpl(
-	 (None,(Ident (Loc.ghost,fname)),None) ,
+	 (None,(Ident (Loc.tag fname)),None) ,
 	 (List.map
 	    (function
 	       | _,Anonymous -> assert false
@@ -480,10 +480,10 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))),
+    Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
-  let eq = Constrexpr_ops.mkCProdN Loc.ghost args unbounded_eq in
+  let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
   let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
       nb_args relation =
     try
@@ -537,13 +537,13 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  let ltof =
 	    let make_dir l = DirPath.make (List.rev_map Id.of_string l) in
-	    Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path
+	    Libnames.Qualid (Loc.tag @@ Libnames.qualid_of_path
 			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
 	  in
 	  let fun_from_mes =
 	    let applied_mes =
 	      Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg])    in
-	    Constrexpr_ops.mkLambdaC ([(Loc.ghost,Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
+	    Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
 	  in
 	  let wf_rel_from_mes =
 	    Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC  ltof,[wf_arg_type;fun_from_mes])
@@ -554,7 +554,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    let a = Names.Id.of_string "___a" in 
 	    let b = Names.Id.of_string "___b" in 
 	    Constrexpr_ops.mkLambdaC(
-	      [Loc.ghost,Name a;Loc.ghost,Name b],
+	      [Loc.tag @@ Name a;Loc.tag @@ Name b],
 	      Constrexpr.Default Explicit,
 	      wf_arg_type,
 	      Constrexpr_ops.mkAppC(wf_rel_expr,
@@ -891,14 +891,14 @@ let make_graph (f_ref:global_reference) =
 			    )
 			in
 			let b' = add_args (snd id) new_args b in
-			((((id,None), ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+			((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
 		     )
 		     fixexprl
 		 in
 		 l
 	     | _ ->
 		let id = Label.to_id (con_label c) in
-		 [(((Loc.ghost,id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+		 [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
 	 let mp,dp,_ = repr_con c in
 	 do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list;
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8f0c986242..de8dc53f11 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -106,7 +106,7 @@ let list_add_set_eq eq_fun x l =
 
 let const_of_id id =
   let _,princ_ref =
-    qualid_of_reference (Libnames.Ident (Loc.ghost,id))
+    qualid_of_reference (Libnames.Ident (Loc.tag id))
   in
   try Constrintern.locate_reference princ_ref
   with Not_found ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8da4f9233e..e4536278c0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -274,7 +274,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       List.map
 	(fun decl ->
 	   List.map
-	     (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
+	     (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id))
 	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
 	)
 	branches
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 9dc1d48df3..f2654b5de8 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -73,7 +73,7 @@ let isVarf f x =
     in global environment. *)
 let ident_global_exist id =
   try
-    let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.ghost,id), None) in
+    let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.tag id), None) in
     let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
     true
   with e when CErrors.noncritical e -> false
@@ -825,7 +825,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let _ = prNamedRConstr (string_of_name nme) tp in
         let _ = prstr "  ;  " in
         let typ = glob_constr_to_constr_expr tp in
-        CLocalAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
+        CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
       [] params in
   let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
   let arity,_ =
@@ -835,7 +835,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let c = RelDecl.get_type decl in
         let typ = Constrextern.extern_constr false env Evd.empty c in
         let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
-        Loc.tag @@ CProdN ([[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
+        Loc.tag @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
       (shift.funresprms2 @ shift.funresprms1
         @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
@@ -849,12 +849,12 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     FIXME: params et cstr_expr (arity) *)
 let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
     (rawlist:(Id.t * glob_constr) list) =
-  let lident = (Loc.ghost, shift.ident), None in
+  let lident = (Loc.tag shift.ident), None in
   let bindlist , cstr_expr = (* params , arities *)
     merge_rec_params_and_arity prms1 prms2 shift mkSet in
   let lcstor_expr : (bool * (lident * constr_expr)) list  =
     List.map (* zeta_normalize t ? *)
-      (fun (id,t) -> false, ((Loc.ghost,id),glob_constr_to_constr_expr t))
+      (fun (id,t) -> false, ((Loc.tag id),glob_constr_to_constr_expr t))
       rawlist in
   lident , bindlist , Some cstr_expr , lcstor_expr
 
@@ -902,7 +902,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
 (* Find infos on identifier id. *)
 let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
   let kn_of_id x =
-    let f_ref = Libnames.Ident (Loc.ghost,x) in
+    let f_ref = Libnames.Ident (Loc.tag x) in
     locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
       locate_constant f_ref in
     try find_Function_infos (kn_of_id id)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 25daedd0e4..9e469c7564 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1306,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     CErrors.error "\"abstract\" cannot handle existentials";
   let hook _ _ =
     let opacity =
-      let na_ref = Libnames.Ident (Loc.ghost,na) in
+      let na_ref = Libnames.Ident (Loc.tag na) in
       let na_global = Smartlocate.global_with_alias na_ref in
       match na_global with
 	  ConstRef c -> is_opaque_constant c
@@ -1556,7 +1556,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let hook _ _ = 
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
-    let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in
+    let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.tag term_id)] in
     (*     message "start second proof"; *)
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);