diff options
| author | Hugo Herbelin | 2020-10-31 14:34:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 16:56:49 +0100 |
| commit | 4814c482eb83f4c21b6ecf2b1b9235b513221181 (patch) | |
| tree | f537790aeba33e55c98e6a3e0ef6cf503fc0197c /engine/evd.mli | |
| parent | 78e600ac5f8aa9609cac4347c7a694428ae9d7cc (diff) | |
Factorizing UState.make* through UState.from_env, to highlight the similarity.
An alternative could also be to split the initialization of the
environment and the declaration of initial "binders".
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index fafaad9a04..40957774fe 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -153,9 +153,9 @@ type evar_map val empty : evar_map (** The empty evar map. *) -val from_env : env -> evar_map +val from_env : ?binders:lident list -> env -> evar_map (** The empty evar map with given universe context, taking its initial - universes from env. *) + universes from env, possibly with initial universe binders. *) val from_ctx : UState.t -> evar_map (** The empty evar map with given universe context *) |