From 70e5fc27679ea515921feea4b5b759303aec1981 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 18 Apr 2011 12:34:11 +0000
Subject: Fix generated script for NMake, a rewrite necessitates full
 conversion for checking types.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14023 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 f095a34821..866bc95b86 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -124,7 +124,7 @@ pr
  revert n. fix IHn 1.
  do 3 (destruct n; [unfold_ops; reflexivity|]).
  simpl mk_zn2z_ops_karatsuba. simpl word in *.
- rewrite <- IHn. auto.
+ rewrite <- (IHn n). auto.
  Qed.
 
  (** * The main type [t], isomorphic with [exists n, word w0 n] *)
-- 
cgit v1.2.3