aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.mli
diff options
context:
space:
mode:
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 5ce16459c..509db525d 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 *)