diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-13 18:43:02 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-13 18:45:41 +0100 |
| commit | c571cdbbcac5cb4b4a5a19ab2f7ac51222316292 (patch) | |
| tree | 2ec7070bc8d58ee4b6fd0734ea41964243a0f2ba /vernac/lemmas.ml | |
| parent | 6bd240fce21c172680a0cec5346b66e08c76418a (diff) | |
[api] Another large deprecation, `Nameops`
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index be9de5b30..7b8a38d5f 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -217,7 +217,7 @@ let compute_proof_name locality = function if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) then - user_err ?loc (pr_id id ++ str " already exists."); + user_err ?loc (Id.print id ++ str " already exists."); id | None -> let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in @@ -294,7 +294,7 @@ let save_anonymous ?export_seff proof save_ident = let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++ + (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ spc () ++ strbrk "declared as an axiom.") let admit (id,k,e) pl hook () = |