diff options
| author | Matthieu Sozeau | 2014-10-15 13:31:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-15 13:34:02 +0200 |
| commit | 6bca54599ab2b8ab928bfc92b8ddfb0aeba4345f (patch) | |
| tree | 9730a7ee84044a8ee5062cc6340cc982b31f7722 /test-suite | |
| parent | 5e1713d8fe9032a3f5c783cce288b409b6fdf816 (diff) | |
Reenable FO unification of primitive projections and their eta-expanded
forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/3484.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3484.v b/test-suite/bugs/closed/3484.v index 3070a4128c..6c40a4266a 100644 --- a/test-suite/bugs/closed/3484.v +++ b/test-suite/bugs/closed/3484.v @@ -14,7 +14,10 @@ Proof. apply (@ap _ _ pr1 _ y). Undo. Unset Printing Notations. - apply (ap pr1). admit. + apply (ap pr1). + Undo. + refine (ap pr1 _). +admit. Defined. (* Toplevel input, characters 22-28: |