Adapt to coq/coq#15754

mit-plv · Mar 20, 2022 · f5fbc4e · f5fbc4e
1 parent 60180c1
commit f5fbc4e
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 34 deletions.
diff --git a/src/Rupicola/Examples/Crypto/Low.v b/src/Rupicola/Examples/Crypto/Low.v
@@ -909,10 +909,10 @@ Notation "'let/n' ( x0 , y0 , z0 , t0 , x1 , y1 , z1 , t1 , x2 , y2 , z2 , t2 ,
                           x2, y2, z2, t2,
                           x3, y3, z3, t3 \> := xyz in body))
     (at level 200,
-      x0 ident, y0 ident, z0 ident, t0 ident,
-      x1 ident, y1 ident, z1 ident, t1 ident,
-      x2 ident, y2 ident, z2 ident, t2 ident,
-      x3 ident, y3 ident, z3 ident, t3 ident,
+      x0 name, y0 name, z0 name, t0 name,
+      x1 name, y1 name, z1 name, t1 name,
+      x2 name, y2 name, z2 name, t2 name,
+      x3 name, y3 name, z3 name, t3 name,
       body at level 200,
       only parsing).
 

diff --git a/src/Rupicola/Examples/Nondeterminism/NonDeterminism.v b/src/Rupicola/Examples/Nondeterminism/NonDeterminism.v
@@ -23,12 +23,12 @@ Import ND.
 
 Notation "'let/+' x 'as' nm := val 'in' body" :=
   (mbindn [nm] val (fun x => body))
-    (at level 200, x ident, body at level 200,
+    (at level 200, x name, body at level 200,
      format "'[hv' 'let/+'  x  'as'  nm  :=  val  'in' '//' body ']'").
 
 Notation "'let/+' x := val 'in' body" :=
   (mbindn [IdentParsing.TC.ident_to_string x] val (fun x => body))
-    (at level 200, x ident, body at level 200,
+    (at level 200, x name, body at level 200,
      only parsing).
 
 Notation "%{ x | P }" :=

diff --git a/src/Rupicola/Lib/Notations.v b/src/Rupicola/Lib/Notations.v
@@ -5,12 +5,12 @@ Require Import Rupicola.Lib.Tactics.
 
 Notation "'let/d' x := val 'in' body" :=
   (dlet val (fun x => body))
-    (at level 200, x ident, body at level 200,
+    (at level 200, x name, body at level 200,
      format "'[hv' 'let/d'  x  :=  '/  ' val  'in'  '/' body ']'").
 
 Notation "'let/d' f a0 .. an := val 'in' body" :=
   (dlet (fun a0 => .. (fun an => val) ..) (fun f => body))
-    (at level 200, f ident, a0 binder, an binder, body at level 200,
+    (at level 200, f name, a0 binder, an binder, body at level 200,
      format "'[hv' 'let/d'  f  a0  ..  an  :=  '/  ' val  'in'  '/' body ']'").
 
 (* TODO: figure out recursive notation for this *)
@@ -52,84 +52,84 @@ Notation nlet_eq_k P v :=
 
 Notation "'let/n' x 'as' nm := val 'in' body" :=
   (nlet [nm] val (fun x => body))
-    (at level 200, x ident, body at level 200,
+    (at level 200, x name, body at level 200,
      format "'[hv' '[' '[' 'let/n'  x  'as'  nm ']'  :=  '/  ' val  'in' ']'  '/' body ']'").
 
 Notation "'let/n' x 'as' nm 'eq:' Heq := val 'in' body" :=
   (nlet_eq [nm] val (fun x Heq => body))
-    (at level 200, x ident, body at level 200,
+    (at level 200, x name, body at level 200,
      format "'[hv' '[' '[' 'let/n'  x  'as'  nm ']'  'eq:' Heq  :=  '/  ' val  'in' ']'  '/' body ']'").
 
 Notation "'let/n' x := val 'in' body" :=
   (nlet [IdentParsing.TC.ident_to_string x] val (fun x => body))
-    (at level 200, x ident, body at level 200,
+    (at level 200, x name, body at level 200,
      only parsing).
 
 Notation "'let/n' x 'eq:' Heq := val 'in' body" :=
   (nlet_eq [IdentParsing.TC.ident_to_string x] val (fun x Heq => body))
-    (at level 200, x ident, body at level 200,
+    (at level 200, x name, body at level 200,
      only parsing).
 
 Notation "'let/n' ( x , y ) 'as' ( nx , ny ) := val 'in' body" :=
   (nlet [nx; ny] val (fun xy => let (x, y) := xy in body))
-    (at level 200, x ident, y ident, body at level 200,
+    (at level 200, x name, y name, body at level 200,
      format "'[hv' '[' '[' 'let/n'  ( x ,  y )  'as'  ( nx ,  ny ) ']'  :=  '/  ' val  'in' ']'  '/' body ']'").
 
 Notation "'let/n' ( x , y ) 'as' ( nx , ny ) 'eq:' Heq := val 'in' body" :=
   (nlet [nx; ny] val (fun xy Heq => let (x, y) := xy in body))
-    (at level 200, x ident, y ident, body at level 200,
+    (at level 200, x name, y name, body at level 200,
      format "'[hv' '[' '[' 'let/n'  ( x ,  y )  'as'  ( nx ,  ny ) ']'  'eq:' Heq  :=  '/  ' val  'in' ']'  '/' body ']'").
 
 Notation "'let/n' ( x , y ) 'eq:' Heq := val 'in' body" :=
   (nlet_eq [IdentParsing.TC.ident_to_string x;
            IdentParsing.TC.ident_to_string y]
            val (fun xy Heq => let (x, y) := xy in body))
-    (at level 200, x ident, y ident, body at level 200,
+    (at level 200, x name, y name, body at level 200,
      only parsing).
 
 Notation "'let/n' ( x , y ) := val 'in' body" :=
   (nlet [IdentParsing.TC.ident_to_string x;
         IdentParsing.TC.ident_to_string y]
         val (fun xy => let (x, y) := xy in body))
-    (at level 200, x ident, y ident, body at level 200,
+    (at level 200, x name, y name, body at level 200,
      only parsing).
 
 (* FIXME generalize using a '\< … \> pattern *)
 
 Notation "'let/n' ( x , y , z ) 'as' ( nx , ny , nz ) := val 'in' body" :=
   (nlet [nx; ny; nz] val (fun xyz => let '\< x, y, z \> := xyz in body))
-    (at level 200, x ident, y ident, z ident, body at level 200,
+    (at level 200, x name, y name, z name, body at level 200,
      format "'[hv' '[' '[' 'let/n'  ( x ,  y ,  z )  'as'  ( nx ,  ny ,  nz ) ']'  :=  '/  ' val  'in' ']'  '/' body ']'").
 
 Notation "'let/n' ( x , y , z ) 'as' ( nx , ny , nz ) 'eq:' Heq := val 'in' body" :=
   (nlet [nx; ny; nz] val (fun xyz Heq => let '\< x, y, z \> := xyz in body))
-    (at level 200, x ident, y ident, z ident, body at level 200,
+    (at level 200, x name, y name, z name, body at level 200,
      format "'[hv' '[' '[' 'let/n'  ( x ,  y ,  z )  'as'  ( nx ,  ny ,  nz ) ']'  'eq:' Heq  :=  '/  ' val  'in' ']'  '/' body ']'").
 
 Notation "'let/n' ( x , y , z ) 'eq:' Heq := val 'in' body" :=
   (nlet_eq [IdentParsing.TC.ident_to_string x;
            IdentParsing.TC.ident_to_string y;
            IdentParsing.TC.ident_to_string z]
            val (fun xyz Heq => let '\< x, y, z \> := xyz in body))
-    (at level 200, x ident, y ident, z ident, body at level 200,
+    (at level 200, x name, y name, z name, body at level 200,
      only parsing).
 
 Notation "'let/n' ( x , y , z ) := val 'in' body" :=
   (nlet [IdentParsing.TC.ident_to_string x;
         IdentParsing.TC.ident_to_string y;
         IdentParsing.TC.ident_to_string z]
         val (fun xyz => let '\< x, y, z \> := xyz in body))
-    (at level 200, x ident, y ident, z ident, body at level 200,
+    (at level 200, x name, y name, z name, body at level 200,
      only parsing).
 
 Notation "'let/n' ( x , y , z , t ) 'as' ( nx , ny , nz , nt ) := val 'in' body" :=
   (nlet [nx; ny; nz; nt] val (fun xyz => let '\< x, y, z, t \> := xyz in body))
-    (at level 200, x ident, y ident, z ident, t ident, body at level 200,
+    (at level 200, x name, y name, z name, t name, body at level 200,
      format "'[hv' '[' '[' 'let/n'  ( x ,  y ,  z ,  t )  'as'  ( nx ,  ny ,  nz ,  nt ) ']'  :=  '/  ' val  'in' ']'  '/' body ']'").
 
 Notation "'let/n' ( x , y , z , t ) 'as' ( nx , ny , nz , nt ) 'eq:' Heq := val 'in' body" :=
   (nlet [nx; ny; nz; nt] val (fun xyz Heq => let '\< x, y, z, t \> := xyz in body))
-    (at level 200, x ident, y ident, z ident, t ident, body at level 200,
+    (at level 200, x name, y name, z name, t name, body at level 200,
      format "'[hv' '[' '[' 'let/n'  ( x ,  y ,  z ,  t )  'as'  ( nx ,  ny ,  nz ,  nt ) ']'  'eq:' Heq  :=  '/  ' val  'in' ']'  '/' body ']'").
 
 Notation "'let/n' ( x , y , z , t ) 'eq:' Heq := val 'in' body" :=
@@ -138,7 +138,7 @@ Notation "'let/n' ( x , y , z , t ) 'eq:' Heq := val 'in' body" :=
            IdentParsing.TC.ident_to_string z;
            IdentParsing.TC.ident_to_string t]
            val (fun xyz Heq => let '\< x, y, z, t \> := xyz in body))
-    (at level 200, x ident, y ident, z ident, t ident, body at level 200,
+    (at level 200, x name, y name, z name, t name, body at level 200,
      only parsing).
 
 Notation "'let/n' ( x , y , z , t ) := val 'in' body" :=
@@ -147,19 +147,19 @@ Notation "'let/n' ( x , y , z , t ) := val 'in' body" :=
         IdentParsing.TC.ident_to_string z;
         IdentParsing.TC.ident_to_string t]
         val (fun xyz => let '\< x, y, z, t \> := xyz in body))
-    (at level 200, x ident, y ident, z ident, t ident, body at level 200,
+    (at level 200, x name, y name, z name, t name, body at level 200,
      only parsing).
 
 Notation "'call!' x" := (Free.Call x) (x at level 200, at level 10).
 
 Notation "'let/!' x 'as' nm := val 'in' body" :=
   (mbindn [nm] val (fun x => body))
-    (at level 200, x ident, body at level 200,
+    (at level 200, x name, body at level 200,
      format "'[hv' '[' '[' 'let/!'  x  'as'  nm ']'  :=  '/  ' val  'in' ']'  '/' body ']'").
 
 Notation "'let/!' x := val 'in' body" :=
   (mbindn [IdentParsing.TC.ident_to_string x] val (fun x => body))
-    (at level 200, x ident, body at level 200,
+    (at level 200, x name, body at level 200,
      only parsing).
 
 (* FIXME add a notation for loops? *)
@@ -236,7 +236,7 @@ Notation "'fnspec!' name a0 .. an '/' g0 .. gn '~>' r0 .. rn ',' '{' 'requires'
      a0 binder, an binder,
      g0 binder, gn binder,
      r0 closed binder, rn closed binder,
-     tr ident, tr' ident, mem ident, mem' ident,
+     tr name, tr' name, mem name, mem' name,
      pre at level 200,
      post at level 200).
 
@@ -256,7 +256,7 @@ Notation "'fnspec!' name a0 .. an '/' g0 .. gn ',' '{' 'requires' tr mem := pre
      name at level 0,
      a0 binder, an binder,
      g0 binder, gn binder,
-     tr ident, tr' ident, mem ident, mem' ident,
+     tr name, tr' name, mem name, mem' name,
      pre at level 200,
      post at level 200).
 
@@ -277,7 +277,7 @@ Notation "'fnspec!' name a0 .. an '~>' r0 .. rn ',' '{' 'requires' tr mem := pre
      name at level 0,
      a0 binder, an binder,
      r0 closed binder, rn closed binder,
-     tr ident, tr' ident, mem ident, mem' ident,
+     tr name, tr' name, mem name, mem' name,
      pre at level 200,
      post at level 200).
 
@@ -295,7 +295,7 @@ Notation "'fnspec!' name '~>' r0 .. rn ',' '{' 'requires' tr mem := pre ';' 'ens
     (at level 200,
      name at level 0,
      r0 closed binder, rn closed binder,
-     tr ident, tr' ident, mem ident, mem' ident,
+     tr name, tr' name, mem name, mem' name,
      pre at level 200,
      post at level 200).
 
@@ -312,7 +312,7 @@ Notation "'fnspec!' name a0 .. an ',' '{' 'requires' tr mem := pre ';' 'ensures'
     (at level 200,
      name at level 0,
      a0 binder, an binder,
-     tr ident, tr' ident, mem ident, mem' ident,
+     tr name, tr' name, mem name, mem' name,
      pre at level 200,
      post at level 200).
 
@@ -328,7 +328,7 @@ Notation "'fnspec!' name '/' g0 .. gn ',' '{' 'requires' tr mem := pre ';' 'ensu
     (at level 200,
      name at level 0,
      g0 binder, gn binder,
-     tr ident, tr' ident, mem ident, mem' ident,
+     tr name, tr' name, mem name, mem' name,
      pre at level 200,
      post at level 200).
 
@@ -347,7 +347,7 @@ Notation "'fnspec!' name a0 .. an '/' g0 .. gn ',' '{' 'requires' tr mem := pre
      name at level 0,
      a0 binder, an binder,
      g0 binder, gn binder,
-     tr ident, tr' ident, mem ident, mem' ident,
+     tr name, tr' name, mem name, mem' name,
      pre at level 200,
      post at level 200).
 
@@ -363,7 +363,7 @@ Notation "'fnspec!' name a0 .. an ',' '{' 'requires' tr mem := pre ';' 'ensures'
     (at level 200,
      name at level 0,
      a0 binder, an binder,
-     tr ident, tr' ident, mem ident, mem' ident,
+     tr name, tr' name, mem name, mem' name,
      pre at level 200,
      post at level 200).