From 46056cbe56f9c39fe3f8f5175aff9fd6427684b6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 5 May 2019 17:11:06 +0200
Subject: Stop using pstate in global print queries

Using pstate makes no sense for printing global stuff
---
 plugins/ssr/ssrvernac.mlg | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 08f028465b..8880a6516e 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -566,12 +566,10 @@ let print_view_hints env sigma kind l =
 }
 
 VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
-| ![proof] [ "Print" "Hint" "View" ssrviewpos(i) ] ->
+| [ "Print" "Hint" "View" ssrviewpos(i) ] ->
   {
-    fun ~pstate ->
-    (* XXX this is incorrect *)
-    let sigma, env = Option.cata Pfedit.get_current_context
-        (let e = Global.env () in Evd.from_env e, e) pstate in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
     (match i with
     | Some k ->
       print_view_hints env sigma k (Ssrview.AdaptorDb.get k)
@@ -579,8 +577,7 @@ VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
         List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k))
           [ Ssrview.AdaptorDb.Forward;
             Ssrview.AdaptorDb.Backward;
-            Ssrview.AdaptorDb.Equivalence ]);
-    pstate
+            Ssrview.AdaptorDb.Equivalence ])
   }
 END
 
-- 
cgit v1.2.3