diff options
| author | Matthieu Sozeau | 2014-07-02 17:19:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-02 17:19:13 +0200 |
| commit | 2ce9f694faf3ea69b0eeb0a5b4214852bcbffc58 (patch) | |
| tree | 5f3a5ebf0b87ab577e85ebd18e835cbb376e3ee5 | |
| parent | c5194d098dce2ab829b63afde4199b750ea85e31 (diff) | |
Fix a Not_found anomaly raised by solve_evar_evar, we were breaking the
invariant that the evar arguments to that function always have to be undefined.
| -rw-r--r-- | pretyping/evarsolve.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 13421bcde4..d15c5d00bd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1159,9 +1159,8 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar ?candidates:evi.evar_candidates (it_mkProd_or_LetIn (mkSort k) ctx) in let evd = Evd.set_leq_sort (Evd.set_leq_sort evd k i) k j in - solve_evar_evar ~force f g env - (solve_evar_evar ~force f g env evd None (ev3,args1) ev1) - pbty (ev3,args1) ev2 + let evd = solve_evar_evar ~force f g env evd (Some false) (ev3,args1) ev1 in + f env evd pbty ev2 (whd_evar evd (mkEvar (ev3,args1))) with Reduction.NotArity -> solve_evar_evar ~force f g env evd None ev1 ev2 |