diff options
| author | Vincent Laporte | 2021-04-19 13:22:05 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2021-04-19 13:22:05 +0200 |
| commit | b53642ec813178fedd3e646832e7c033b8163f52 (patch) | |
| tree | e93f364cec8238a4f95ebbe48e84dda5606eea07 /theories | |
| parent | f82dd4e968d1b948f4288687cb9458ec90b66270 (diff) | |
| parent | d2c7022f0e16e6037c0d8c30c837abaad2c8194f (diff) | |
Merge PR #14108: [zify] bugfix
Reviewed-by: Zimmi48
Reviewed-by: vbgl
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/micromega/ZifyClasses.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index 019d11d951..25d9fa9104 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -7,7 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Set Primitive Projections. (** An alternative to [zify] in ML parametrised by user-provided classes instances. @@ -220,6 +219,13 @@ Proof. exact (fun H => proj1 IFF H). Qed. +Lemma rew_iff_rev (P Q : Prop) (IFF : P <-> Q) : Q -> P. +Proof. + exact (fun H => proj2 IFF H). +Qed. + + + (** Registering constants for use by the plugin *) Register eq_iff as ZifyClasses.eq_iff. Register target_prop as ZifyClasses.target_prop. @@ -247,6 +253,7 @@ Register eq as ZifyClasses.eq. Register mkinjprop as ZifyClasses.mkinjprop. Register iff_refl as ZifyClasses.iff_refl. Register rew_iff as ZifyClasses.rew_iff. +Register rew_iff_rev as ZifyClasses.rew_iff_rev. Register source_prop as ZifyClasses.source_prop. Register injprop_ok as ZifyClasses.injprop_ok. Register iff as ZifyClasses.iff. |