diff options
| author | Alix Trieu <atrieu@users.noreply.github.com> | 2019-04-09 16:41:34 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-04-15 14:54:54 +0200 |
| commit | b2965fa033073c46fbc0e27900598a88580d2197 (patch) | |
| tree | f85b775503da3054ead957b03fe1b7fdc5c9cb64 | |
| parent | 7361c01f5df99e36f700b8257115fc96f2fff779 (diff) | |
| download | compcert-b2965fa033073c46fbc0e27900598a88580d2197.tar.gz compcert-b2965fa033073c46fbc0e27900598a88580d2197.zip | |
Fix typo in section name in Selectionproof.v
SEL_SWITH_INT -> SEL_SWITCH_INT
| -rw-r--r-- | backend/Selectionproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index dc01ad20..afc470b3 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -460,7 +460,7 @@ Qed. End SEL_SWITCH. -Section SEL_SWITH_INT. +Section SEL_SWITCH_INT. Variable cunit: Cminor.program. Variable hf: helper_functions. @@ -547,7 +547,7 @@ Proof. - apply Int64.unsigned_range. Qed. -End SEL_SWITH_INT. +End SEL_SWITCH_INT. (** Compatibility of evaluation functions with the "less defined than" relation. *) |