aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_global.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_global.mli')
-rw-r--r--proofs/proof_global.mli2
1 files changed, 1 insertions, 1 deletions
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