Skip to content

Commit 1ffde91

Browse files
committed
Fix position of some comments
1 parent fa78921 commit 1ffde91

File tree

6 files changed

+11
-11
lines changed

6 files changed

+11
-11
lines changed

compiler/backend/clos_knownScript.sml

+2-2
Original file line numberDiff line numberDiff line change
@@ -281,8 +281,8 @@ Datatype:
281281
| Tuple num (val_approx list) (* conses or tuples *)
282282
| Int int (* used to index tuples *)
283283
| Other (* unknown *)
284-
| Impossible
285-
End (* value 'returned' by Raise *)
284+
| Impossible (* value 'returned' by Raise *)
285+
End
286286
val val_approx_size_def = definition "val_approx_size_def"
287287

288288
Definition merge_def[nocompute]:

compiler/backend/gc/gen_gc_partialScript.sml

+2-2
Original file line numberDiff line numberDiff line change
@@ -238,8 +238,8 @@ End
238238

239239
Datatype:
240240
data_sort = Protected 'a (* pointer to old generations *)
241-
| Real 'b
242-
End (* data or pointer to current generation *)
241+
| Real 'b (* data or pointer to current generation *)
242+
End
243243

244244
Definition to_gen_heap_address_def:
245245
(to_gen_heap_address conf (Data a) = Data (Real a)) /\

compiler/backend/reg_alloc/reg_allocScript.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -1009,8 +1009,8 @@ Datatype:
10091009
| Set num_set (* Fixed set *)
10101010
| Branch (num_set option) clash_tree clash_tree
10111011
| Seq clash_tree clash_tree
1012-
End
10131012
(* Binary branch, with an optional liveset at the head*)
1013+
End
10141014

10151015
(* --- clash_tree oracle checks --- *)
10161016
Definition numset_list_delete_def:

compiler/backend/wordLangScript.sml

+2-2
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,8 @@ Datatype:
5555
| CodeBufferWrite num num (* code buffer address, byte to write *)
5656
| DataBufferWrite num num (* data buffer address, word to write *)
5757
| FFI string num num num num num_set (* FFI name, conf_ptr, conf_len, array_ptr, array_len, cut-set *)
58-
| ShareInst memop num ('a exp)
59-
End (* memory operation, varname, expression for memory address *)
58+
| ShareInst memop num ('a exp) (* memory operation, varname, expression for memory address *)
59+
End
6060

6161
Definition raise_stub_location_def:
6262
raise_stub_location = word_num_stubs - 2

examples/lpr_checker/lprScript.sml

+2-2
Original file line numberDiff line numberDiff line change
@@ -1166,8 +1166,8 @@ QED
11661166
Datatype:
11671167
step =
11681168
Del cclause (* Clause to delete *)
1169-
| Add cclause
1170-
End (* Clause to add *)
1169+
| Add cclause (* Clause to add *)
1170+
End
11711171

11721172
Type proof = ``:step list``
11731173

translator/monadic/examples/array_searchProgScript.sml

+2-2
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ fun allowing_rebind f = Feedback.trace ("Theory.allow_rebinds", 1) f
1111

1212
(* Create the data type to handle the array. *)
1313
Datatype:
14-
state_array = <| arr : num list |>
15-
End (* single resizeable array *)
14+
state_array = <| arr : num list |> (* single resizeable array *)
15+
End
1616

1717
(* Data type for the exceptions *)
1818
Datatype:

0 commit comments

Comments
 (0)