diff options
author | 2017-11-21 22:24:59 +0100 | |
---|---|---|
committer | 2017-11-21 22:24:59 +0100 | |
commit | eb91ccaf236bc9a60a1e216b76a0a42980c072a7 (patch) | |
tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc /plugins/ssr/ssrvernac.ml4 | |
parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
parent | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (diff) |
Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.
Diffstat (limited to 'plugins/ssr/ssrvernac.ml4')
-rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 36dce37ae..cd614fee9 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -343,7 +343,7 @@ let coerce_search_pattern_to_sort hpat = let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in let warn () = Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ - pr_constr_pattern hpat') in + pr_constr_pattern_env env sigma hpat') in if EConstr.isSort sigma ht then begin warn (); true, hpat' end else let filter_head, coe_path = try @@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat = let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr coe ++ spc () + errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path @@ -468,10 +468,12 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function prc c ++ str "|" ++ int (List.length args) | c -> prc c -let pr_rawhintref c = match DAst.get c with +let pr_rawhintref c = + let _, env = Pfedit.get_current_context () in + match DAst.get c with | GApp (f, args) when isRHoles args -> - pr_glob_constr f ++ str "|" ++ int (List.length args) - | _ -> pr_glob_constr c + pr_glob_constr_env env f ++ str "|" ++ int (List.length args) + | _ -> pr_glob_constr_env env c let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c |