diff options
| author | Maxime Dénès | 2018-12-22 02:04:26 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-24 16:46:17 +0100 |
| commit | 309cf3d3d6fe57ba9c15c32872b42433596c7748 (patch) | |
| tree | bfe48784396347d1081f4342de4bcca2afe4b397 /plugins/nsatz | |
| parent | 1006fd52c03e7d8ea1d0b612df168f21c9b56455 (diff) | |
Make `Instance` without a body always open a proof.
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index c5a09d677e..a964febf9c 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -452,6 +452,7 @@ constructor;red;intros;subst;trivial. Qed. Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)). +Defined. Instance Rri : (Ring (Ro:=Rops)). constructor; @@ -468,6 +469,7 @@ 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). +Defined. Lemma R_one_zero: 1%R <> 0%R. discrR. @@ -484,6 +486,7 @@ exact Rmult_integral. exact R_one_zero. Defined. Require Import QArith. Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). +Defined. Instance Qri : (Ring (Ro:=Qops)). constructor. |