diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/evars.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 69f7164c7a..52c4f2daad 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -254,3 +254,7 @@ Proof. (* error message with V8.3 : Impossible to unify "?18" with "fun g : nat -> nat => ?6 = g". *) Abort. + +(* Regression test *) + +Definition fo : option nat -> nat := option_rec _ (fun a => 0) 0. |