diff options
Diffstat (limited to 'plugins/nsatz/Nsatz.v')
| -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. |