diff options
Diffstat (limited to 'theories/Logic/Eqdep_dec.v')
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index ea5b16517..9bde2d641 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -101,7 +101,7 @@ Section EqdepDec. Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x := match exP with - | ex_intro x' prf => + | ex_intro _ x' prf => match eq_dec x' x with | or_introl eqprf => eq_ind x' P prf x eqprf | _ => def |