diff options
| author | Pierre-Marie Pédrot | 2020-04-27 21:53:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-27 21:53:57 +0200 |
| commit | d15b99d93b67f37a0c572950868713b2a7a2b1a4 (patch) | |
| tree | e332379083cd993e343ac0995ab207963315a401 /test-suite | |
| parent | 2781da7585c56b836093940d7337cf18c4146faf (diff) | |
| parent | 087804f288e82a5e4538b7b2387bdc324bebe7b6 (diff) | |
Merge PR #12073: Split off Nsatz tactic part into Nsatz_tactic
Reviewed-by: anton-trunov
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_5359.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_5445.v | 11 |
2 files changed, 13 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. diff --git a/test-suite/bugs/closed/bug_5445.v b/test-suite/bugs/closed/bug_5445.v new file mode 100644 index 0000000000..deaf174661 --- /dev/null +++ b/test-suite/bugs/closed/bug_5445.v @@ -0,0 +1,11 @@ +Require Import Coq.nsatz.NsatzTactic. +(** Ensure that loading the nsatz tactic doesn't load the reals *) +Fail Module M := Coq.Reals.Rdefinitions. +(** Ensure that loading the nsatz tactic doesn't load classic *) +Fail Check Coq.Logic.Classical_Prop.classic. +(** Ensure that this test-case hasn't messed up about the location of the reals / how to check for them *) +Require Coq.Reals.Rdefinitions. +Module M := Coq.Reals.Rdefinitions. +(** Ensure that this test-case hasn't messed up about the location of classic / how to check for it *) +Require Coq.Logic.Classical_Prop. +Check Coq.Logic.Classical_Prop.classic. |