diff options
| author | Jasper Hugunin | 2020-08-22 16:00:32 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:31 -0700 |
| commit | 20b6715c5172a4483c52b743ead2ed53eb82e7d6 (patch) | |
| tree | 194962d186ff608cefac221e185a2edbe0873eca | |
| parent | d6b1274515890c22930ae54ff0b7bb492eebd622 (diff) | |
Modify Init/Tactics.v to compile with -mangle-names
| -rw-r--r-- | theories/Init/Tactics.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index b13206db94..6b4551318b 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -203,7 +203,7 @@ Set Implicit Arguments. Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}), C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide. Proof. - intros; destruct decide. + intros C decide H P H0; destruct decide. - apply H0. - contradiction. Qed. @@ -211,7 +211,7 @@ Qed. Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}), ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide. Proof. - intros; destruct decide. + intros C decide H P H0; destruct decide. - contradiction. - apply H0. Qed. |