diff options
| author | Enrico Tassi | 2019-01-29 16:22:41 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-29 16:22:41 +0100 |
| commit | 325c4ae65f5c72c531a18b1d3871c840a2f32980 (patch) | |
| tree | 0783ae991ce01a9d9b7ffbc520bba0d1ca8502db /plugins/nsatz | |
| parent | a9b141469fe3036355be95d8cf5f0bf5c240fe37 (diff) | |
| parent | 309cf3d3d6fe57ba9c15c32872b42433596c7748 (diff) | |
Merge PR #9274: Make `Instance` without a body always open a proof
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: ppedrot
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. |