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.ml | |
| 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.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f92110ea5..2e215b605 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -333,8 +333,8 @@ let check_evars_are_solved env current_sigma frozen pending = (* Try typeclasses, hooks, unification heuristics ... *) -let solve_remaining_evars flags env current_sigma pending = - let frozen,pending = frozen_and_pending_holes pending in +let solve_remaining_evars flags env current_sigma init_sigma = + let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in let evdref = ref current_sigma in if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then @@ -343,12 +343,12 @@ let solve_remaining_evars flags env current_sigma pending = if flags.fail_evar then check_evars_are_solved env !evdref frozen pending; !evdref -let check_evars_are_solved env current_sigma pending = - let frozen,pending = frozen_and_pending_holes pending in +let check_evars_are_solved env current_sigma init_sigma = + let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in check_evars_are_solved env current_sigma frozen pending let process_inference_flags flags env initial_sigma (sigma,c) = - let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in + let sigma = solve_remaining_evars flags env sigma initial_sigma in let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c |