diff options
| author | Jasper Hugunin | 2020-12-15 20:45:50 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2020-12-15 20:45:50 -0800 |
| commit | 4c4fb148fa874da2065501d70f757c27685957cd (patch) | |
| tree | 5ac6e8fb6622415c74f987369d7c1dbfba086cae | |
| parent | 0f8d5745a3edd428aa5677880b5dcc5077f5b91b (diff) | |
Modify Bool/BoolEq.v to compile with -mangle-names
| -rw-r--r-- | theories/Bool/BoolEq.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index f002ee427c..dd10c758a5 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -46,7 +46,7 @@ Section Bool_eq_dec. Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}. Proof. - intros. + intros x y. exists (beq x y). constructor. Defined. |