From ddbb9bae3d82547aa57db8e9d44010f7c73ce10f Mon Sep 17 00:00:00 2001 From: Andrej Dudenhefner Date: Fri, 10 May 2024 15:29:56 +0200 Subject: [PATCH] improve performance of TM/Single/StepTM.v --- theories/TM/Single/StepTM.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/TM/Single/StepTM.v b/theories/TM/Single/StepTM.v index f78d5a18..d9fcccb8 100644 --- a/theories/TM/Single/StepTM.v +++ b/theories/TM/Single/StepTM.v @@ -384,7 +384,7 @@ Section ToSingleTape. Notation nMax := (finMax' n). Local Arguments finMax' : simpl never. - Notation sigSim := (FinType(EqType(boundary + sigList (sigTape sig)))). + Definition sigSim := (FinType(EqType(boundary + sigList (sigTape sig)))). Implicit Types (T : tapes sig n).