diff options
| author | Gaëtan Gilbert | 2019-05-05 17:11:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-24 16:23:32 +0200 |
| commit | 46056cbe56f9c39fe3f8f5175aff9fd6427684b6 (patch) | |
| tree | 9c70ee243a2f5025bea4f7c8306d7cbd25f5d66f /plugins/ssr | |
| parent | 831639deec0ce88fca4ede4756815cf434088ac3 (diff) | |
Stop using pstate in global print queries
Using pstate makes no sense for printing global stuff
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 11 |
1 files changed, 4 insertions, 7 deletions
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 |