diff options
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e9d3e782b..ecb36615f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -232,7 +232,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** Gather the universes transitively used in the term, including in the type of evars appearing in it. *) -val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t +val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t (** {6 Substitutions} *) @@ -321,7 +321,7 @@ sig val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt (** Physical identity. Does not care for defined evars. *) - val to_named_context : (t, types) Context.Named.pt -> Context.Named.t + val to_named_context : (t, types) Context.Named.pt -> Constr.named_context val to_sorts : ESorts.t -> Sorts.t (** Physical identity. Does not care for normalization. *) |