Deprecate parse

theories/Parser.v

@@ -141,14 +141,18 @@ Arguments until        {_ _ _}.
 Arguments untilMulti   {_ _ _}.
 
 Definition parse' {T} (p: parser T) (acc: list ascii) (str: string)
-  : option string + T * list ascii :=
-  match runStateT p (acc ++ list_ascii_of_string str)%list with
-  | inl e  => inl e
-  | inr sl => inr sl
+  : (option string + T) * list ascii :=
+  let input : list ascii := (acc ++ list_ascii_of_string str)%list in
+  match runStateT p input with
+  | inl e  => (inl e, input)
+  | inr (s, l) => (inr s, l)
   end.
 
-Definition parse {T} (p: parser T) (str: string) : option string + T * string :=
+Definition deprecated_parse {T} (p: parser T) (str: string) : option string + T * string :=
   match parse' p [] str with
-  | inl e      => inl e
-  | inr (s, l) => inr (s, string_of_list_ascii l)
+  | (inl e, _) => inl e
+  | (inr res, remainder) => inr (res, string_of_list_ascii remainder)
   end.
+
+#[deprecated(note="Use parse' instead")]
+Notation parse := deprecated_parse.