From 150f799caadc33efb600f7a3799f6a57d0c598c0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Oct 2024 10:00:47 +0200 Subject: [PATCH] remove buggy notation --- HB/structures.v | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/HB/structures.v b/HB/structures.v index 8b2bf7b5e..2c64060e4 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -1208,15 +1208,5 @@ Notation "`Error_cannot_unify: t1 'with' t2" := (unify t1 t2 None) Notation "`Error: t msg T" := (unify t _ (Some (msg%string, T))) (at level 0, msg, T at level 0, format "`Error: t msg T", only printing) : form_scope. - -Notation "[find v | t1 ∼ t2 ] rest" := - (fun v (_ : unify t1 t2 None) => rest) (at level 0, only parsing) : - form_scope. -Notation "[find v1, .., vn | t1 ∼ t2 ] rest" := - (fun v1 .. vn => fun (_ : unify t1 t2 None) => rest) (at level 0, only parsing) : - form_scope. -Notation "[find v | t1 ∼ t2 | msg ] rest" := - (fun v (_ : unify t1 t2 (Some msg)) => rest) (at level 0, only parsing) : - form_scope. - + Global Open Scope string_scope.