diff options
| author | Maxime Dénès | 2017-10-25 10:16:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-25 10:16:57 +0200 |
| commit | ad973248998da8d7d10ed00f4bcd6f383ba9a171 (patch) | |
| tree | 705a2b2de824b39d97a28fcea3b8287b53204b54 /printing | |
| parent | 7d2dfd6fabd5d447166b1cb0e3b2993cc8abf4b3 (diff) | |
| parent | 069ab52e2af900d498395ebd1b00b7983152326e (diff) | |
Merge PR #6009: Master+misc typos dead code etc
Diffstat (limited to 'printing')
| -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 2077526db4..fdaeded878 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 |