diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-04-20 17:50:10 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-04-20 17:50:10 +0200 |
| commit | 9354722485c71ba6fbe6e6462eae98113aa830cc (patch) | |
| tree | f2a8718cc534196262049183bbf3084e97a4a232 /plugins/nsatz | |
| parent | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (diff) | |
Fix nsatz not recognizing real literals.
Diffstat (limited to 'plugins/nsatz')
| -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 b11d15e5c..403f664e2 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. |