diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 5 | ||||
| -rw-r--r-- | printing/printmod.ml | 5 |
2 files changed, 4 insertions, 6 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f371fb08c7..10dd42ea91 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -718,10 +718,7 @@ open Decl_kinds match o with | None -> (match opac with | Transparent -> keyword "Defined" - | Opaque None -> keyword "Qed" - | Opaque (Some l) -> - keyword "Qed" ++ spc() ++ str"export" ++ - prlist_with_sep (fun () -> str", ") pr_lident l) + | Opaque -> keyword "Qed") | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id ) | VernacExactProof c -> diff --git a/printing/printmod.ml b/printing/printmod.ml index 219eafda4c..755e905a70 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -64,9 +64,10 @@ let get_new_id locals id = if not (Nametab.exists_module dir) then id else - get_id (id::l) (Namegen.next_ident_away id l) + get_id (Id.Set.add id l) (Namegen.next_ident_away id l) in - get_id (List.map snd locals) id + let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in + get_id avoid id (** Inductive declarations *) |