From 40dee46e5f119d6642a5dc7661778746aff25580 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 Jun 2010 22:53:02 +0000
Subject: Fixing commit r13090 (forgot to commit the file generating
 Nmake_gen.v).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13095 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Natural/BigN/NMake_gen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 0c15950edc..fb182720c9 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -365,7 +365,7 @@ pr "
 
   pp " Instance wn_spec (n:nat) : ZnZ.Specs (make_op n).";
   pp " Proof.";
-  pp "  intros n; elim n; clear n.";
+  pp "  elim n; clear n.";
   pp "    exact w%i_spec." (size + 1);
   pp "  intros n Hrec; rewrite make_op_S.";
   pp "  exact (mk_zn2z_specs_karatsuba Hrec).";
-- 
cgit v1.2.3