diff options
| author | Jasper Hugunin | 2021-01-08 12:38:47 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2021-01-08 12:38:47 -0800 |
| commit | 76cbd4afbeb13d97852e97e805c0e1890eae1d6c (patch) | |
| tree | b5edfce9345023f441844d6003ebee6a53bf415e /theories/Program | |
| parent | afed8dcf54d7a9e8e8ac04e4ec2de1784270e2e4 (diff) | |
Modify Program/Subset.v to compile with -mangle-names
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. |