aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.mli
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 /engine/evd.mli
parent87c959542e1bed55b14d371f1be02cd60d89082c (diff)
parentafceace455a4b37ced7e29175ca3424996195f7b (diff)
Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Diffstat (limited to 'engine/evd.mli')
-rw-r--r--engine/evd.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index 5ce16459c2..509db525d9 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -649,7 +649,7 @@ val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> eva
val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
- evar_map -> Globnames.global_reference -> evar_map * econstr
+ evar_map -> GlobRef.t -> evar_map * econstr
(********************************************************************)
(* constr with holes and pending resolution of classes, conversion *)