Commit d731cb31 authored by Ralf Jung's avatar Ralf Jung

fix comment

parent 815b0180
......@@ -5,7 +5,7 @@ From iris_examples.logatom.lib Require Export gc.
Set Default Proof Using "Type".
(** A general logically atomic interface for RDCSS.
See [rdcss.v] for references and more details about this data structure. *)
See [rdcss.v] for references and more details about this data structure.
_Note on the use of GC locations_: the specification of the [rdcss] operation
as given by [rdcss_spec] relies on the [gc_mapsto l_m m] assertion. It roughly
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment