diff options
Diffstat (limited to 'mathcomp/ssreflect/plugin/trunk')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 0e04221..d214dc3 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 |