From de9aafba67f888e1de7921b951d422c864a868a7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 25 Nov 2015 19:23:34 +0100
Subject: fix: Hint View is not a Query

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 +-
 mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/ssreflect/plugin')

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
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index e6636cb..d5d7bf3 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
-- 
cgit v1.2.3