diff options
| author | Hugo Herbelin | 2020-03-22 12:30:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-03 20:33:27 +0200 |
| commit | aa889ee516453af65bd74ffedf8ec3761f97eb43 (patch) | |
| tree | 9dbe0527c1fc7dd34eb8fa9a2462d3a96048baaa /theories/PArith | |
| parent | 9e98c1ebb9472f1c77eb0289bd64e525d58d99de (diff) | |
Avoiding using a fixed introduction name in Ltac code of stdlib.
Diffstat (limited to 'theories/PArith')
| -rw-r--r-- | theories/PArith/BinPos.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 387ab75362..4179765dca 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1753,7 +1753,7 @@ Qed. Ltac destr_pggcdn IHn := match goal with |- context [ ggcdn _ ?x ?y ] => - generalize (IHn x y); destruct ggcdn as (g,(u,v)); simpl + generalize (IHn x y); destruct ggcdn as (?g,(?u,?v)); simpl end. Lemma ggcdn_correct_divisors : forall n a b, |