diff options
Diffstat (limited to 'ia32/Asmgenproof1.v')
-rw-r--r-- | ia32/Asmgenproof1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 9ddc4639..5d3df679 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -97,7 +97,7 @@ Ltac Simplifs := repeat Simplif. Section CONSTRUCTORS. Variable ge: genv. -Variable fn: code. +Variable fn: function. (** Smart constructor for moves. *) |