diff options
Diffstat (limited to 'theories/Logic/Eqdep_dec.v')
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index f362eb23ca..96c8f91c95 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -20,11 +20,10 @@ (* We need some dependent elimination schemes *) -Scheme eq_indd := Induction for eq Sort Prop. -Scheme eqT_indd := Induction for eqT Sort Prop. -Scheme or_indd := Induction for or Sort Prop. -Implicit Arguments On. +Set Implicit Arguments. + +Require Elimdep. (* Bijection between [eq] and [eqT] *) Definition eq2eqT: (A:Set)(x,y:A)x=y->x==y := |