diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-22 19:06:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-23 11:54:48 +0100 |
| commit | 8cfe40dbc02156228a529c01190c50d825495013 (patch) | |
| tree | f40da159fed52eb9db479180bd323d59ba9245df /pretyping/pretyping.mli | |
| parent | 8b73fd7c6ce423f8c8a2594e90200f2407795d52 (diff) | |
Ensuring static invariants about handling of pending evars in Pretyping.
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 2c6aa7a21..23957d557 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -129,13 +129,13 @@ val type_uconstr : [pending], however, it can contain more evars than the pending ones. *) val solve_remaining_evars : inference_flags -> - env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map + env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map (** Checking evars and pending conversion problems are all solved, reporting an appropriate error message *) val check_evars_are_solved : - env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit + env -> (* current map: *) evar_map -> (* initial map: *) evar_map -> unit (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) |