diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 19:08:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-21 18:04:32 +0100 |
| commit | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (patch) | |
| tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc /tactics/inv.ml | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
[printing] Deprecate all printing functions accessing the global proof.
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 8648dfb90..46b10bf33 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -282,10 +282,11 @@ let generalizeRewriteIntros as_mode tac depids id = let error_too_many_names pats = let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ?loc ( str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ - str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ + str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ str ".") let get_names (allow_conj,issimple) (loc, pat as x) = match pat with |