diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-18 12:34:11 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-18 12:34:11 +0000 |
| commit | 70e5fc27679ea515921feea4b5b759303aec1981 (patch) | |
| tree | 459654a462041a1ec85c9b657d7e2d27f1a26af9 /theories/Numbers | |
| parent | 092cb84f074112ab9b33f936d5a79d58102c9eec (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')
| -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 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] *) |