diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-18 16:30:29 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-18 16:30:29 +0000 |
| commit | 2a18ccc965df83c592917e5d20e938bce196eca8 (patch) | |
| tree | e37f8ea2f331a03e34330273313f39a8e221a6a7 /theories/Logic/Eqdep_dec.v | |
| parent | 6d8328ec5e7dad8d5347cce5d7ce5a699381671c (diff) | |
Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1790 85f007b7-540e-0410-9357-904b9bb8a0f7
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 f362eb23c..96c8f91c9 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 := |