diff options
| author | Cyril Cohen | 2020-11-19 18:33:21 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-19 21:38:46 +0100 |
| commit | e565f8d9bebd4fd681c34086d5448dbaebc11976 (patch) | |
| tree | 3e74907bf8e310b6400b7c340357ad44fc44a83f /mathcomp/ssreflect/finfun.v | |
| parent | 0dbefe01e54a467b7932a514355f0435b4cfb978 (diff) | |
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/ssreflect/finfun.v')
| -rw-r--r-- | mathcomp/ssreflect/finfun.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 0218f6a..1fd1a83 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -175,7 +175,7 @@ Proof. suffices ffunK f g: (forall x, f x = g x) -> f = finfun g. by split=> [/ffunK|] -> //; apply/esym/ffunK. case: f => f Dg; rewrite unlock; congr FinfunOf. -have{Dg} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx. +have{} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx. by rewrite -Dg /= (bool_irrelevance (mem_enum _ _) aTx). elim: (enum aT) / f (enum_uniq aT) => //= x1 s y f IHf /andP[s'x1 Us] in Dg *. rewrite Dg ?eqxx //=; case: eqP => // /eq_axiomK-> /= _. |