diff options
| author | coqbot-app[bot] | 2021-03-19 07:49:21 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-19 07:49:21 +0000 |
| commit | be64fe07ec2bcf5177bb227813d8f896ef00c265 (patch) | |
| tree | 8aaa4bf16e7bb462f50e89354692df7c9f11adda /theories/Program | |
| parent | eeef63b0b09cf90f7a3022ce6f0d7e50a908484c (diff) | |
| parent | 06c816527a26a9e9e09601b67c128b381c4bd2af (diff) | |
Merge PR #13730: Lint stdlib with -mangle-names #6
Reviewed-by: anton-trunov
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Subset.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 9788ad50dc..9540bc1075 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -68,10 +68,11 @@ Ltac pi := repeat f_equal ; apply proof_irrelevance. Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m. Proof. + intros A P n m. destruct n as (x,p). destruct m as (x',p'). simpl. - split ; intros ; subst. + split ; intros H ; subst. - inversion H. reflexivity. @@ -92,7 +93,7 @@ Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B) (y : {y:A | y = x}), match_eq A B x fn = fn y. Proof. - intros. + intros A B x fn y. unfold match_eq. f_equal. destruct y. |