diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_8848.v | 18 |
2 files changed, 21 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 diff --git a/test-suite/bugs/closed/bug_8848.v b/test-suite/bugs/closed/bug_8848.v new file mode 100644 index 0000000000..26563e6747 --- /dev/null +++ b/test-suite/bugs/closed/bug_8848.v @@ -0,0 +1,18 @@ +Require Import Program. +Set Implicit Arguments. +Unset Strict Implicit. + +Definition def (a : nat) := a = a. + +Structure record {a : nat} {D : def a} := + inR { prop : Prop }. + +Program +Canonical Structure ins (a : nat) (rec : @record a _) := + @inR a _ (prop rec). +Next Obligation. + exact eq_refl. +Defined. +Next Obligation. + exact eq_refl. +Defined. |