diff options
| -rw-r--r-- | test-suite/bugs/closed/3043.v | 3 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 8 |
2 files changed, 7 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/3043.v b/test-suite/bugs/closed/3043.v new file mode 100644 index 000000000..12885987f --- /dev/null +++ b/test-suite/bugs/closed/3043.v @@ -0,0 +1,3 @@ +Goal (fun A (P : A -> Prop) (X : sigT P) => proj1_sig X) = (fun A (P : A -> Prop) (X : sigT P) => projT1 X). + reflexivity. +Qed. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 88c2c264a..ee8111639 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -107,11 +107,11 @@ End Projections. (** [sigT] of a predicate is equivalent to [sig] *) -Lemma sig_of_sigT : forall (A:Type) (P:A->Prop), sigT P -> sig P. -Proof. destruct 1 as (x,H); exists x; trivial. Defined. +Definition sig_of_sigT (A : Type) (P : A -> Prop) (X : sigT P) : sig P + := exist P (projT1 X) (projT2 X). -Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P. -Proof. destruct 1 as (x,H); exists x; trivial. Defined. +Definition sigT_of_sig (A : Type) (P : A -> Prop) (X : sig P) : sigT P + := existT P (proj1_sig X) (proj2_sig X). Coercion sigT_of_sig : sig >-> sigT. Coercion sig_of_sigT : sigT >-> sig. |