From bb5dab84859088d70074444cfbf0e51f14e3c782 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 23 Apr 2021 18:29:20 +0200
Subject: Move `$` notation in submodule `ClightNotations` and scope
 `clight_scope`

This avoids a nasty conflict with Ltac2 notations as reported in #392.

The old `$` notation in scope `string_scope` was not used yet, AFAIK.

The new submodule and the new scope are the right places to add future
notations to facilitate working with the output of clightgen.

Fixes: #392
---
 exportclight/Clightdefs.v | 34 +++++++++++++++++++++++-----------
 1 file changed, 23 insertions(+), 11 deletions(-)

(limited to 'exportclight')

diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index 8af920df..f96513d1 100644
--- a/exportclight/Clightdefs.v
+++ b/exportclight/Clightdefs.v
@@ -18,6 +18,8 @@
 From Coq Require Import Ascii String List ZArith.
 From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight.
 
+(** ** Short names for types *)
+
 Definition tvoid := Tvoid.
 Definition tschar := Tint I8 Signed noattr.
 Definition tuchar := Tint I8 Unsigned noattr.
@@ -56,6 +58,8 @@ Definition talignas (n: N) (ty: type) :=
 Definition tvolatile_alignas (n: N) (ty: type) :=
   tattr {| attr_volatile := true; attr_alignas := Some n |} ty.
 
+(** ** Constructor for programs and compilation units *)
+
 Definition wf_composites (types: list composite_definition) : Prop :=
   match build_composite_env types with OK _ => True | Error _ => False end.
 
@@ -81,6 +85,8 @@ Definition mkprogram (types: list composite_definition)
      prog_comp_env := ce;
      prog_comp_env_eq := EQ |}.
 
+(** ** Encoding character strings as positive numbers *)
+
 (** The following encoding of character strings as positive numbers
     must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *)
 
@@ -169,17 +175,6 @@ Fixpoint ident_of_string (s: string) : ident :=
   | String c s => append_char_pos c (ident_of_string s)
   end.
 
-(** A convenient notation [$ "ident"] to force evaluation of
-    [ident_of_string "ident"] *)
-
-Ltac ident_of_string s :=
-  let x := constr:(ident_of_string s) in
-  let y := eval compute in x in
-  exact y.
-
-Notation "$ s" := (ltac:(ident_of_string s))
-                  (at level 1, only parsing) : string_scope.
-
 (** The inverse conversion, from encoded strings to strings *)
 
 Section DECODE_BITS.
@@ -289,3 +284,20 @@ Proof.
   intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2).
   congruence.
 Qed.
+
+(** ** Notations *)
+
+Module ClightNotations.
+
+(** A convenient notation [$ "ident"] to force evaluation of
+    [ident_of_string "ident"] *)
+
+Ltac ident_of_string s :=
+  let x := constr:(ident_of_string s) in
+  let y := eval compute in x in
+  exact y.
+
+Notation "$ s" := (ltac:(ident_of_string s))
+                  (at level 1, only parsing) : clight_scope.
+
+End ClightNotations.
-- 
cgit