diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 0e04221048..d214dc3235 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -2397,7 +2397,7 @@ let glob_view_hints lvh = let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh)) -VERNAC COMMAND EXTEND HintView CLASSIFIED AS QUERY +VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF | [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] -> [ mapviewpos (add_view_hints (glob_view_hints lvh)) n 2 ] END diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 index e6636cb5e2..d5d7bf316c 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 @@ -2391,7 +2391,7 @@ let glob_view_hints lvh = let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh)) -VERNAC COMMAND EXTEND HintView CLASSIFIED AS QUERY +VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF | [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] -> [ mapviewpos (add_view_hints (glob_view_hints lvh)) n 2 ] END