From 8831588462fbf0cdbbb12c5000afe23895f6d498 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 7 Jul 2017 13:22:12 +0200
Subject: [PATCH] Anonymize.

---
 theories/lang/notation.v                   | 2 +-
 theories/lang/races.v                      | 2 +-
 theories/lifetime/model/primitive.v        | 2 --
 theories/typing/lib/refcell/refcell_code.v | 2 +-
 4 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 8057d97f..01f30578 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -93,7 +93,7 @@ Notation "'letcall:' x := f args 'in' e" :=
   (letcont: "_k" [ x ] := e in call: f args → "_k")%E
   (at level 102, x, f, args at level 1, e at level 150) : expr_scope.
 
-(* RJ: These notations unfortunately do not print.  Also, I don't think
+(* These notations unfortunately do not print.  Also, I don't think
    we would even want them to print in general.
    TODO: Introduce a Definition. *)
 Notation "e1 '<-{Σ' i } '()'" := (e1 <- #i)%E
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 3321b135..647f112b 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -118,7 +118,7 @@ Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' a1 a2 l :
 Proof.
   intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_head_step;
   destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
-  (* Oh my. FIXME RJ. *)
+  (* Oh my. FIXME. *)
   - eapply lit_neq_state; last done.
     setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
     cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 41e689c1..5f77eea2 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -498,8 +498,6 @@ Proof.
   iApply ("Hvs" $! I'' with "Hinv HPb H†").
 Qed.
 
-(* TODO RJ: Are there still places where this lemma
-   is re-proven inline? *)
 Lemma lft_vs_cons κ Pb Pb' Pi :
   (lft_bor_dead κ -∗ ▷ Pb'-∗ [†κ] ={↑borN}=∗ lft_bor_dead κ ∗ ▷ Pb) -∗
   lft_vs κ Pb Pi -∗ lft_vs κ Pb' Pi.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 58e80365..e596aca9 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -49,7 +49,7 @@ Section refcell_functions.
     funrec: <> ["x"] :=
       let: "r" := new [ #ty.(ty_size)] in
       "r" <-{ty.(ty_size)} !("x" +â‚— #1);;
-          (* TODO RJ: Can we make it so that the parenthesis above are mandatory?
+          (* TODO: Can we make it so that the parenthesis above are mandatory?
              Leaving them away is inconsistent with `let ... := !"x" +â‚— #1`. *)
        delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
 
-- 
GitLab