Skip to content

Commit

Permalink
Merge pull request #610 from gares/quickfix-deprecated
Browse files Browse the repository at this point in the history
adapt to coq/coq#19300
  • Loading branch information
ppedrot committed Jul 8, 2024
2 parents 6dd6383 + b4dbc59 commit abed609
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -258,7 +258,7 @@ let tactic_parser : qualid Attributes.key_parser = fun ?loc orig args ->
assert_once ?loc ~name:"tactic" orig;
match args with
| VernacFlagLeaf (FlagString str) -> qualid_of_string str
| VernacFlagLeaf (FlagIdent str) -> qualid_of_string str
| VernacFlagLeaf (FlagQualid q) -> q
| _ -> CErrors.user_err ?loc (Pp.str "Ill formed \"tactic\" attribute")
let equations_tactic =
Attributes.attribute_of_list ["tactic",tactic_parser]
Expand Down

0 comments on commit abed609

Please sign in to comment.