aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
authorMaxime Dénès2018-05-06 17:19:58 +0200
committerMaxime Dénès2018-05-06 17:19:58 +0200
commitdad4731deed5c09e4e6cb212cd81462f7896c363 (patch)
tree413c52bbb7c67c228e20434ef2dfd6bd59c86753 /plugins/ltac
parent87c959542e1bed55b14d371f1be02cd60d89082c (diff)
parentafceace455a4b37ced7e29175ca3424996195f7b (diff)
Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/taccoerce.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 1fa5e3c076..5185217cda 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -80,7 +80,7 @@ val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t
val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list
-val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> Globnames.global_reference
+val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> GlobRef.t
val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis