diff options
| author | Maxime Dénès | 2016-07-08 13:03:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-08 13:03:16 +0200 |
| commit | e1661dc9a43b34526437e9bc3029e6320e09f899 (patch) | |
| tree | 9378bcab7bbff366e4c87c56e490fbd6ccb5010c | |
| parent | b0e81d65b85c1846a961196d70cd86ede2993c5b (diff) | |
Fix test file for #4858.
| -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 c04895a1bb..a2fa93832a 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). |