aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-18 12:34:11 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-18 12:34:11 +0000
commit70e5fc27679ea515921feea4b5b759303aec1981 (patch)
tree459654a462041a1ec85c9b657d7e2d27f1a26af9 /theories/Numbers/Natural
parent092cb84f074112ab9b33f936d5a79d58102c9eec (diff)
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
Diffstat (limited to 'theories/Numbers/Natural')
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml2
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 f095a3482..866bc95b8 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] *)