diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-18 15:46:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:28:53 +0200 |
| commit | e8a6467545c2814c9418889201e8be19c0cef201 (patch) | |
| tree | 7f513d854b76b02f52f98ee0e87052c376175a0f /proofs | |
| parent | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff) | |
[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.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 8367c09b8..b9c925796 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 f9fb0b76d..89aa32643 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 d659eba24..32eb9a3c1 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 6bb6f5e2c..b0b0eba08 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 |