diff options
| author | Maxime Dénès | 2017-04-25 07:59:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-25 07:59:13 +0200 |
| commit | 97db512af4888da529e641f71539adef444cb8e3 (patch) | |
| tree | bf90fc28312d4f182d139680faf274f1b5a795f5 /plugins | |
| parent | e57074289193b0f0184f3c7143d8ab7e0edd5112 (diff) | |
| parent | 9354722485c71ba6fbe6e6462eae98113aa830cc (diff) | |
Merge PR#578: Fix nsatz not recognizing real literals.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index b11d15e5ca..403f664e2b 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -462,6 +462,11 @@ try (try apply Rsth; exact Rplus_opp_r. Defined. +Class can_compute_Z (z : Z) := dummy_can_compute_Z : True. +Hint Extern 0 (can_compute_Z ?v) => + match isZcst v with true => exact I end : typeclass_instances. +Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z). + Lemma R_one_zero: 1%R <> 0%R. discrR. Qed. |