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 96e4b6acc..7576b3d5f 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -580,7 +580,7 @@ val update_sigma_env : evar_map -> env -> evar_map
(** Polymorphic universes *)
val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
-val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant
+val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant
val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor