From 127e9da1c160032eff67a1c174182a98f6b51ebc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 17 Jan 2019 15:21:07 -0500 Subject: Remove ? notation It was colliding with the ?[a] notation for fresh evars --- src/Util/Strings/ParseArithmetic.v | 1 - 1 file changed, 1 deletion(-) (limited to 'src/Util') diff --git a/src/Util/Strings/ParseArithmetic.v b/src/Util/Strings/ParseArithmetic.v index 2ae6ea347..5e58c838a 100644 --- a/src/Util/Strings/ParseArithmetic.v +++ b/src/Util/Strings/ParseArithmetic.v @@ -97,7 +97,6 @@ Global Arguments orelse {A%type} (parse parse')%parse s%string. Local Open Scope parse_scope. Notation "a <- parse_A ; parse_B" := (bind_parse parse_A%parse (fun a => parse_B%parse)) : parse_scope. -Notation "?" := maybe_parse : parse_scope. Infix "||" := orelse : parse_scope. Fixpoint parse_Z (s : string) : option (Z * string) -- cgit v1.2.3