diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-08 13:03:16 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-08 13:03:16 +0200 |
| commit | e1661dc9a43b34526437e9bc3029e6320e09f899 (patch) | |
| tree | 9378bcab7bbff366e4c87c56e490fbd6ccb5010c /test-suite/bugs/closed/4858.v | |
| parent | b0e81d65b85c1846a961196d70cd86ede2993c5b (diff) | |
Fix test file for #4858.
Diffstat (limited to 'test-suite/bugs/closed/4858.v')
| -rw-r--r-- | test-suite/bugs/closed/4858.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v index c04895a1b..a2fa93832 100644 --- a/test-suite/bugs/closed/4858.v +++ b/test-suite/bugs/closed/4858.v @@ -1,6 +1,6 @@ Require Import Nsatz. Goal True. -nsatz_compute +try nsatz_compute (PEc 0%Z :: PEc (-1)%Z :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1 :: PEsub (PEX Z 1) (PEX Z 1) :: nil). |