From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 18 Jan 2017 15:46:23 +0100
Subject: [location] Make location optional in Loc.located

This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.

We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.

The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
---
 proofs/evar_refiner.ml  | 2 +-
 proofs/pfedit.mli       | 2 +-
 proofs/proof_global.ml  | 2 +-
 proofs/proof_global.mli | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 8367c09b8f..b9c9257969 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -56,7 +56,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
-      user_err ~loc 
+      user_err ?loc 
                 (str "Instance is not well-typed in the environment of " ++
                  Termops.pr_existential_key sigma evk ++ str ".")
   in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f9fb0b76de..89aa32643b 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -130,7 +130,7 @@ val set_end_tac : Genarg.glob_generic_argument -> unit
 (** [set_used_variables l] declares that section variables [l] will be
     used in the proof *)
 val set_used_variables :
-  Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list
+  Id.t list -> Context.Named.t * Names.Id.t Loc.located list
 val get_used_variables : unit -> Context.Named.t option
 
 (** {6 Universe binders } *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d659eba240..32eb9a3c1a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -207,7 +207,7 @@ let discard (loc,id) =
   let n = List.length !pstates in
   discard_gen id;
   if Int.equal (List.length !pstates) n then
-    CErrors.user_err ~loc
+    CErrors.user_err ?loc
       ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6bb6f5e2cb..b0b0eba08d 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -140,7 +140,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
 val set_used_variables :
-  Names.Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list
+  Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list
 val get_used_variables : unit -> Context.Named.t option
 
 val get_universe_binders : unit -> universe_binders option
-- 
cgit v1.2.3