diff options
| author | Jasper Hugunin | 2020-12-15 20:51:29 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2020-12-15 20:51:29 -0800 |
| commit | 29c881414cf1ae7c6c882c1285f72b5d5cba1b4e (patch) | |
| tree | 903466462b53ff4fe1018511453b4de91e27f342 | |
| parent | 511a81ab5826ecf2f0eae2447da7a3f83b660003 (diff) | |
Modify Classes/DecidableClass.v to compile with -mangle-names
| -rw-r--r-- | theories/Classes/DecidableClass.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v index 7169aa673d..cd6765bab9 100644 --- a/theories/Classes/DecidableClass.v +++ b/theories/Classes/DecidableClass.v @@ -46,7 +46,7 @@ Qed. (** The generic function that should be used to program, together with some useful tactics. *) -Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). +Definition decide P {H : Decidable P} := @Decidable_witness _ H. Ltac _decide_ P H := let b := fresh "b" in |