diff options
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 713d6f233..6b607c38d 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -600,7 +600,7 @@ ARGUMENT EXTEND opthints | [ ] -> [ None ] END -VERNAC COMMAND EXTEND HintCut +VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ let entry = HintsCutEntry p in Auto.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) |