diff options
| author | Pierre-Marie Pédrot | 2018-10-31 01:01:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-31 01:01:21 +0100 |
| commit | 20752cb329262ddb4b4a9ba898fd8566bf5ad156 (patch) | |
| tree | a0c04fd5ad497f97697ea182d38bd76234721270 /pretyping | |
| parent | d32301dde8071acc914286c675b9749e27f368d2 (diff) | |
| parent | 57a0d5091a9524d35161875a884835a573d82e0b (diff) | |
Merge PR #8849: Fix for bug #8848.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 674f6846ae..dd38ec6f64 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1240,9 +1240,9 @@ let check_evar_instance evd evk1 body conv_algo = let update_evar_info ev1 ev2 evd = (* We update the source of obligation evars during evar-evar unifications. *) - let loc, evs2 = evar_source ev2 evd in - let evi = Evd.find evd ev1 in - Evd.add evd ev1 {evi with evar_source = loc, evs2} + let loc, evs1 = evar_source ev1 evd in + let evi = Evd.find evd ev2 in + Evd.add evd ev2 {evi with evar_source = loc, evs1} let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = try |