diff options
| author | Enrico Tassi | 2019-03-04 15:17:34 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-26 14:09:41 +0100 |
| commit | b4561c5047eb2383c2b718fd1cf9da8076497511 (patch) | |
| tree | 086a1b3bcecbd42beb7f5436542be0f470dc60d4 /test-suite | |
| parent | a59d80d3d482813b3c3c1ebce18ae39c3d09e5be (diff) | |
[evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663)
In particular evar_eqappr_x tries to find a miller pattern on both sides,
while the fast path for evars tries solve_simple_eqn in one direction
only. So if you have (Evar-not-miller = Evar-miller) the code was not
trying to solve the RHS.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_9663.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9663.v b/test-suite/bugs/closed/bug_9663.v new file mode 100644 index 0000000000..b5fa601278 --- /dev/null +++ b/test-suite/bugs/closed/bug_9663.v @@ -0,0 +1,2 @@ +Definition id_depfn S T (f : forall x : S, T x) := f. +Definition idn : nat -> nat := @id_depfn _ _ (fun x => x). |