aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.mli')
-rw-r--r--proofs/pfedit.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7622a8776..1bf65b8ae 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 } *)