diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-04 19:37:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-24 11:14:13 +0200 |
| commit | e29948c5606bfcab182cf0f325750fdb3215856e (patch) | |
| tree | 78341a2923103244e083fed73c58e21606f5d73c /printing/prettyp.ml | |
| parent | 341dcf85e43bd2569910426cfbcdc28032dfdb68 (diff) | |
An occurrence of set_id which behaves as the identity.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 2077526db..fdaeded87 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -807,7 +807,8 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - str |> Global.lookup_named |> NamedDecl.set_id str |> print_named_decl + str |> Global.lookup_named |> print_named_decl + with Not_found -> user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") @@ -839,7 +840,7 @@ let print_opaque_name qid = let open EConstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl + env |> lookup_named id |> print_named_decl let print_about_any ?loc k = match k with |