From 20c8d28f9f7c5818bdfc32081900f915293d5928 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 7 Dec 2023 17:54:59 +0100 Subject: [PATCH] Adapt to math-comp/math-comp#1133 (replace fun_scope with function_scope) --- src/spec/operations.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/spec/operations.v b/src/spec/operations.v index f8ed452..28f7ea3 100644 --- a/src/spec/operations.v +++ b/src/spec/operations.v @@ -76,7 +76,7 @@ Notation carry_addB p1 p2 := (adcB false p1 p2).1. Notation addB p1 p2 := (adcB false p1 p2).2. (* Take a page from ssreflect's book of ssrfun *) Notation "@ 'addB' n" := (fun p1 p2 : BITS n => addB p1 p2) - (at level 10, n at level 8, only parsing) : fun_scope. + (at level 10, n at level 8, only parsing) : function_scope. (*(** Don't simpl unless everything is a constructor. *) Global Arguments adcB {!n} !carry !p1 !p2 / .*) @@ -105,7 +105,7 @@ Definition sbbB {n} borrow (arg1 arg2: BITS n) := Notation carry_subB p1 p2 := (sbbB false p1 p2).1. Notation subB p1 p2 := (sbbB false p1 p2).2. Notation "@ 'subB' n" := (fun p1 p2 : BITS n => subB p1 p2) - (at level 10, n at level 8, only parsing) : fun_scope. + (at level 10, n at level 8, only parsing) : function_scope. (** Don't ever simpl [sbbB]. *) (*Global Arguments sbbB {!n} !borrow !arg1 !arg2 / .*)