diff options
| author | Jason Gross | 2020-04-19 16:18:22 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-04-24 17:28:54 -0400 |
| commit | 087804f288e82a5e4538b7b2387bdc324bebe7b6 (patch) | |
| tree | e6dcf4b05879f92528b5dc65193699ccb5fb4fe3 /test-suite | |
| parent | 1b258168882c17f2afed9e25d51732013bafa184 (diff) | |
Make the nsatz test-suite pass
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_5359.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_5359.v b/test-suite/bugs/closed/bug_5359.v index 1f202e4396..36f2ec5891 100644 --- a/test-suite/bugs/closed/bug_5359.v +++ b/test-suite/bugs/closed/bug_5359.v @@ -90,7 +90,7 @@ Goal False. (Ring_polynom.PEX Z 2))) (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) (Ring_polynom.PEX Z 3)))) :: nil)%list ) in - Nsatz.nsatz_compute + NsatzTactic.nsatz_compute (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))). let sugar := constr:( 0%Z ) in @@ -214,6 +214,6 @@ Goal False. (Ring_polynom.PEX Z 2))) (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) (Ring_polynom.PEX Z 3)))) :: nil)%list ) in - Nsatz.nsatz_compute + NsatzTactic.nsatz_compute (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))). Abort. |