diff options
| author | Jasper Hugunin | 2021-01-08 14:01:55 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2021-01-08 14:01:55 -0800 |
| commit | 8241077c681bb48a0b413e4ee68961f0684b0294 (patch) | |
| tree | 88842b8b81ca4a5e0fd8736e0e03f6680755b2fb /theories | |
| parent | e2850002db0271aff914c6a81d17354991b0d5cb (diff) | |
Modify Classes/SetoidDec.v to compile with -mangle-names
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Classes/SetoidDec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 2947c4831f..f4220e3aa1 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -96,7 +96,7 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) := Next Obligation. Proof. - destruct x ; destruct y. + do 2 match goal with x : () |- _ => destruct x end. reflexivity. Qed. |