diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 14 | ||||
| -rw-r--r-- | printing/printer.ml | 52 |
2 files changed, 37 insertions, 29 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f71719cb9a..37098e5042 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -27,6 +27,10 @@ open Recordops open Misctypes open Printer open Printmod +open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : mutual_inductive -> std_ppcmds; @@ -132,7 +136,6 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in - let open Context.Rel.Declaration in let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in @@ -170,9 +173,8 @@ type opacity = | TransparentMaybeOpacified of Conv_oracle.level let opacity env = - let open Context.Named.Declaration in function - | VarRef v when is_local_def (Environ.lookup_named v env) -> + | VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) | ConstRef cst -> @@ -733,8 +735,7 @@ 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; - let open Context.Named.Declaration in - str |> Global.lookup_named |> set_id str |> print_named_decl + str |> Global.lookup_named |> NamedDecl.set_id str |> print_named_decl with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") @@ -762,8 +763,7 @@ let print_opaque_name qid = let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let open Context.Named.Declaration in - lookup_named id env |> set_id id |> print_named_decl + lookup_named id env |> NamedDecl.set_id id |> print_named_decl let print_about_any loc k = match k with diff --git a/printing/printer.ml b/printing/printer.ml index 28fd92659e..5c62c2af0e 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -22,6 +22,10 @@ open Constrextern open Ppconstr open Declarations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration +module NamedListDecl = Context.NamedList.Declaration + let emacs_str s = if !Flags.print_emacs then s else "" let delayed_emacs_cmd s = @@ -248,31 +252,36 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (**********************************************************************) (* Contexts and declarations *) -let pr_var_decl_skel pr_id env sigma (id,c,typ) = - let pbody = match c with - | None -> (mt ()) - | Some c -> - (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in - let pb = if isCast c then surround pb else pb in - (str" := " ++ pb ++ cut () ) in +let pr_var_list_decl env sigma decl = + let ids, pbody, typ = match decl with + | NamedListDecl.LocalAssum (ids, typ) -> + ids, mt (), typ + | NamedListDecl.LocalDef (ids,c,typ) -> + (* Force evaluation *) + let pb = pr_lconstr_env env sigma c in + let pb = if isCast c then surround pb else pb in + ids, (str" := " ++ pb ++ cut ()), typ + in + let pids = prlist_with_sep pr_comma pr_id ids in let pt = pr_ltype_env env sigma typ in let ptyp = (str" : " ++ pt) in - (pr_id id ++ hov 0 (pbody ++ ptyp)) - -let pr_var_decl env sigma d = - pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d) - -let pr_var_list_decl env sigma (l,c,typ) = - hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) + hov 0 (pids ++ pbody ++ ptyp) + +let pr_var_decl env sigma decl = + let decl = match decl with + | NamedDecl.LocalAssum (id, t) -> + NamedListDecl.LocalAssum ([id], t) + | NamedDecl.LocalDef (id,c,t) -> + NamedListDecl.LocalDef ([id],c,t) + in + pr_var_list_decl env sigma decl let pr_rel_decl env sigma decl = - let open Context.Rel.Declaration in - let na = get_name decl in - let typ = get_type decl in + let na = RelDecl.get_name decl in + let typ = RelDecl.get_type decl in let pbody = match decl with - | LocalAssum _ -> mt () - | LocalDef (_,c,_) -> + | RelDecl.LocalAssum _ -> mt () + | RelDecl.LocalDef (_,c,_) -> (* Force evaluation *) let pb = pr_lconstr_env env sigma c in let pb = if isCast c then surround pb else pb in @@ -417,8 +426,7 @@ let pr_evgl_sign sigma evi = | None -> [], [] | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) in - let open Context.Named.Declaration in - let ids = List.rev_map get_id l in + let ids = List.rev_map NamedDecl.get_id l in let warn = if List.is_empty ids then mt () else (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") |