From 5650c8a32282f4ae5e3938500ee0cf1e36fdd620 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 21 Jun 2025 15:16:58 +0200 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/17876 --- vfa-current/Trie.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/vfa-current/Trie.v b/vfa-current/Trie.v index 80108cd54..4ac1f9317 100644 --- a/vfa-current/Trie.v +++ b/vfa-current/Trie.v @@ -169,10 +169,8 @@ Eval compute in print_in_binary ten. (* = [1; 0; 1; 0] *) (** Another way to see the "binary representation" is to make up postfix notation for [xI] and [xO], as follows *) -Notation "p ~ 1" := (xI p) - (at level 7, left associativity, format "p '~' '1'"). -Notation "p ~ 0" := (xO p) - (at level 7, left associativity, format "p '~' '0'"). +Notation "p ~ 1" := (xI p). +Notation "p ~ 0" := (xO p). Print ten. (* = xH~0~1~0 : positive *)