diff --git a/theories/TM/Util/TM_facts.v b/theories/TM/Util/TM_facts.v index e8cfb165..68e3a145 100644 --- a/theories/TM/Util/TM_facts.v +++ b/theories/TM/Util/TM_facts.v @@ -249,7 +249,7 @@ Proof. erewrite VectorSpec.nth_map2; eauto. Qed. (* Set Notation scopes for tapes, so that the alphabet of the tape is parsed as a type (e.g. [X+Y] is parsed as the sum type, not the addition of [X] and [Y]) *) -Arguments tapes (sig %__ type) (n %__ nat). +Arguments tapes (sig %_ type) (n %_ nat). (* ** Nop Action *)