diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-07-31 16:49:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-09-19 10:28:03 +0200 |
| commit | 8966c9241207b6f5d4ee38508246ee97ed006e72 (patch) | |
| tree | 774d61f09e653e084c9fc1c1b5fd01996ab09a76 /engine/evd.mli | |
| parent | d9e54d65cc808eab2908beb7a7a2c96005118ace (diff) | |
proof_global: cleanup and comment close_proof
evd: Move constrain_variables to an operation on UState
Necessary to check universe declarations correctly for deferred proofs
in particular.
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 76fa69e31..8c3771cd9 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context val evar_universe_context_of_binders : |