Remove sugar for [value<v>].

ANNOTATIONS.md

@@ -545,7 +545,6 @@ There is some special support for predefined type constructors:
    does not have to deal with this directly, but there are cases where this is
    necessary. For example, when recursive occurences of a type appear undear
    an `array` type.
- - `value<v>` is sugar for `value<LPtr, v>`.
 
 # Annotations using macros
 

frontend/coq_pp.ml

@@ -625,15 +625,6 @@ and pp_type_expr_guard : unit pp option -> guard_mode -> type_expr pp =
                   Panic.panic_no_pos "[%s] expects exactly one argument." id
             in
             fprintf ff "guarded %a %a" with_uid s (pp_arg true true) ty;
-        | "value"                  ->
-            let (ly, v) =
-              match tyas with
-              | [v]     -> (Ty_arg_expr(Ty_Coq(Coq_ident("void*"))), v)
-              | [ly; v] -> (ly                                    , v)
-              | _       ->
-                  Panic.panic_no_pos "[%s] expects one or two argument." id
-            in
-            fprintf ff "value %a %a" (pp_arg true true) ly (pp_arg true true) v
         | _                        ->
             default ()
   and pp_arg wrap guarded ff tya =

theories/typing/singleton.v

@@ -104,7 +104,6 @@ Section value.
 
 End value.
 Notation "value< ly , v >" := (value ly v) (only printing, format "'value<' ly ',' v '>'") : printing_sugar.
-Notation "value< v >" := (value void* v) (only printing, format "'value<' v '>'") : printing_sugar.
 
 Section place.
   Context `{!typeG Σ}.

tutorial/proofs/t03_list/generated_proof_length_val.v

@@ -17,7 +17,7 @@ Section proof_length_val.
       <[ "#1" :=
         ∃ v2 : val,
         ∃ l1 : list type,
-        arg_p ◁ₗ (own_constrained (nonshr_constraint (v2 ◁ᵥ l1 @ list_t)) (value void* (v2))) ∗
+        arg_p ◁ₗ (own_constrained (nonshr_constraint (v2 ◁ᵥ l1 @ list_t)) (value (void*) (v2))) ∗
         local_len ◁ₗ ((length l - length l1) @ (int (size_t))) ∗
         (v ◁ᵥ (wand_val (void*) (v2 ◁ᵥ l1 @ list_t) (l @ (list_t))))
     ]> $

tutorial/proofs/t03_list/generated_spec.v

@@ -129,12 +129,12 @@ Section spec.
 
   (* Specifications for function [length_val_rec]. *)
   Definition type_of_length_val_rec :=
-    fn(∀ (v, l) : val * (list type); (value void* (v)); (v ◁ᵥ (l @ (list_t))) ∗ ⌜length l <= max_int size_t⌝)
+    fn(∀ (v, l) : val * (list type); (value (void*) (v)); (v ◁ᵥ (l @ (list_t))) ∗ ⌜length l <= max_int size_t⌝)
       → ∃ () : (), ((length l) @ (int (size_t))); (v ◁ᵥ (l @ (list_t))).
 
   (* Specifications for function [length_val]. *)
   Definition type_of_length_val :=
-    fn(∀ (v, l) : val * (list type); (value void* (v)); (v ◁ᵥ l @ list_t) ∗ ⌜length l <= max_int size_t⌝)
+    fn(∀ (v, l) : val * (list type); (value (void*) (v)); (v ◁ᵥ l @ list_t) ∗ ⌜length l <= max_int size_t⌝)
       → ∃ () : (), ((length l) @ (int (size_t))); (v ◁ᵥ l @ list_t).
 
   (* Specifications for function [append]. *)

tutorial/t03_list.c

@@ -98,7 +98,7 @@ size_t length (list_t *p) {
 }
 
 [[rc::parameters("v : val", "l : {list type}")]]
-[[rc::args("value<v>")]]
+[[rc::args("value<void*,v>")]]
 [[rc::requires("v : l @ list_t")]]
 [[rc::requires("{length l <= max_int size_t}")]]
 [[rc::returns("{length l} @ int<size_t>")]]
@@ -111,7 +111,7 @@ size_t length_val_rec (list_t p) {
 }
 
 [[rc::parameters("v : val", "l : {list type}")]]
-[[rc::args("value<v>")]]
+[[rc::args("value<void*,v>")]]
 [[rc::requires("[v ◁ᵥ l @ list_t]")]]
 [[rc::requires("{length l <= max_int size_t}")]]
 [[rc::returns("{length l} @ int<size_t>")]]
@@ -119,7 +119,7 @@ size_t length_val_rec (list_t p) {
 size_t length_val (list_t p) {
   size_t len = 0;
   [[rc::exists("v2 : val", "l1 : {list type}")]]
-  [[rc::inv_vars("p : own_constrained<nonshr_constraint<{v2 ◁ᵥ l1 @ list_t}>, value<v2>>",
+  [[rc::inv_vars("p : own_constrained<nonshr_constraint<{v2 ◁ᵥ l1 @ list_t}>, value<void*,v2>>",
                  "len : {length l - length l1} @ int<size_t>")]]
   [[rc::constraints("v : wand_val<void*, {v2 ◁ᵥ l1 @ list_t}, l @ list_t>")]]
   while (p != NULL) {