diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 534b680e2..0baba94c6 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -765,7 +765,7 @@ let _ = pp " Ltac zg_tac := try"; pp " (red; simpl Zcompare; auto;"; - pp " let t := fresh \"H\" in (intros t; discriminate H))."; + pp " let t := fresh \"H\" in (intros t; discriminate t))."; pp " Lemma spec_iter: forall x y, P [x] [y] (iter x y)."; pp " Proof."; pp " intros x; case x; clear x; unfold iter."; |