diff options
| author | Pierre-Marie Pédrot | 2019-08-27 17:09:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-08-27 17:09:49 +0200 |
| commit | 07078458b164ba54decd6c6e9bd059d1d1b6ec8f (patch) | |
| tree | 39494b1228d47f01e61544725abfea0b694c22b2 /theories | |
| parent | 1e1d5bf3879424688fa9231ba057b05d86674d22 (diff) | |
| parent | 979991789a4adec7d55322b1e997911b0f6fae81 (diff) | |
Merge PR #10680: Tauto: use Coqlib to locate “not” and “NNPP”
Reviewed-by: ppedrot
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/Classical_Prop.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index 6af7b1fe6e..9c47b73193 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -26,6 +26,8 @@ unfold not; intros; elim (classic p); auto. intro NP; elim (H NP). Qed. +Register NNPP as core.nnpp.type. + (** Peirce's law states [forall P Q:Prop, ((P -> Q) -> P) -> P]. Thanks to [forall P, False -> P], it is equivalent to the following form *) |