diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 55 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 10 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 10 | ||||
| -rw-r--r-- | printing/prettyp.ml | 25 | ||||
| -rw-r--r-- | printing/prettyp.mli | 8 | ||||
| -rw-r--r-- | printing/printer.ml | 45 | ||||
| -rw-r--r-- | printing/printer.mli | 13 | ||||
| -rw-r--r-- | printing/printmod.ml | 4 |
8 files changed, 94 insertions, 76 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d92d832759..38eeda9b96 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -317,9 +317,9 @@ let tag_var = tag Tag.variable pr_sep_com spc (pr ltop) rhs)) let begin_of_binder = function - LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) - | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) - | LocalPattern(loc,_,_) -> fst (Loc.unloc loc) + | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc) + | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) + | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false let begin_of_binders = function @@ -360,15 +360,13 @@ let tag_var = tag Tag.variable hov 1 (if many then surround_impl b s else surround_implicit b s) let pr_binder_among_many pr_c = function - | LocalRawAssum (nal,k,t) -> + | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) - | LocalRawDef (na,c) -> - let c,topt = match c with - | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t - | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in - surround (pr_lname na ++ pr_opt_type pr_c topt ++ - str":=" ++ cut() ++ pr_c c) - | LocalPattern (loc,p,tyo) -> + | CLocalDef (na,c,topt) -> + surround (pr_lname na ++ + pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ + str" :=" ++ spc() ++ pr_c c) + | CLocalPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -382,9 +380,9 @@ let tag_var = tag Tag.variable let pr_delimited_binders kw sep pr_c bl = let n = begin_of_binders bl in match bl with - | [LocalRawAssum (nal,k,t)] -> + | [CLocalAssum (nal,k,t)] -> kw n ++ pr_binder false pr_c (nal,k,t) - | (LocalRawAssum _ | LocalPattern _) :: _ as bdl -> + | (CLocalAssum _ | CLocalPattern _) :: _ as bdl -> kw n ++ pr_undelimited_binders sep pr_c bdl | _ -> assert false @@ -395,33 +393,33 @@ let tag_var = tag Tag.variable let rec extract_prod_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_prod_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) | CProdN (loc,[],c) -> extract_prod_binders c | CProdN (loc,[[_,Name id],bk,t], CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in - LocalPattern (loc,p,None) :: bl, c + CLocalPattern (loc,p,None) :: bl, c | CProdN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c + CLocalAssum (nal,bk,t) :: bl, c | c -> [], c let rec extract_lam_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_lam_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) | CLambdaN (loc,[],c) -> extract_lam_binders c | CLambdaN (loc,[[_,Name id],bk,t], CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in - LocalPattern (loc,p,None) :: bl, c + CLocalPattern (loc,p,None) :: bl, c | CLambdaN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c + CLocalAssum (nal,bk,t) :: bl, c | c -> [], c let split_lambda = function @@ -450,7 +448,7 @@ let tag_var = tag Tag.variable let (na,_,def) = split_lambda def in let (na,t,typ) = split_product na typ in let (bl,typ,def) = split_fix (n-1) typ def in - (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def) + (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def) let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = @@ -467,9 +465,9 @@ let tag_var = tag Tag.variable match (ro : Constrexpr.recursion_order_expr) with | CStructRec -> let names_of_binder = function - | LocalRawAssum (nal,_,_) -> nal - | LocalRawDef (_,_) -> [] - | LocalPattern _ -> assert false + | CLocalAssum (nal,_,_) -> nal + | CLocalDef (_,_,_) -> [] + | CLocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" @@ -588,7 +586,7 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) + | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -598,11 +596,12 @@ let tag_var = tag Tag.variable pr spc ltop b), lletin ) - | CLetIn (_,x,a,b) -> + | CLetIn (_,x,a,t,b) -> return ( hv 0 ( - hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :=" - ++ pr spc ltop a ++ spc () + hov 2 (keyword "let" ++ spc () ++ pr_lname x + ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr mt ltop t) t + ++ str " :=" ++ pr spc ltop a ++ spc () ++ keyword "in") ++ pr spc ltop b), lletin @@ -703,7 +702,7 @@ let tag_var = tag Tag.variable | CEvar (_,n,l) -> return (pr_evar (pr mt) n l, latom) | CPatVar (_,p) -> - return (str "?" ++ pr_patvar p, latom) + return (str "@?" ++ pr_patvar p, latom) | CSort (_,s) -> return (pr_glob_sort s, latom) | CCast (_,a,b) -> diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index a0106837ad..f92caf426e 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -19,12 +19,12 @@ open Names open Misctypes val extract_lam_binders : - constr_expr -> local_binder list * constr_expr + constr_expr -> local_binder_expr list * constr_expr val extract_prod_binders : - constr_expr -> local_binder list * constr_expr + constr_expr -> local_binder_expr list * constr_expr val split_fix : int -> constr_expr -> constr_expr -> - local_binder list * constr_expr * constr_expr + local_binder_expr list * constr_expr * constr_expr val prec_less : int -> int * Ppextend.parenRelation -> bool @@ -50,12 +50,12 @@ val pr_patvar : patvar -> std_ppcmds val pr_glob_level : glob_level -> std_ppcmds val pr_glob_sort : glob_sort -> std_ppcmds val pr_guard_annot : (constr_expr -> std_ppcmds) -> - local_binder list -> + local_binder_expr list -> ('a * Names.Id.t) option * recursion_order_expr -> std_ppcmds val pr_record_body : (reference * constr_expr) list -> std_ppcmds -val pr_binders : local_binder list -> std_ppcmds +val pr_binders : local_binder_expr list -> std_ppcmds val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds val pr_constr_expr : constr_expr -> std_ppcmds diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 78ef4d4bad..cfc2e48d11 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -534,18 +534,8 @@ open Decl_kinds (* Stm *) | VernacStm JoinDocument -> return (keyword "Stm JoinDocument") - | VernacStm PrintDag -> - return (keyword "Stm PrintDag") - | VernacStm Finish -> - return (keyword "Stm Finish") | VernacStm Wait -> return (keyword "Stm Wait") - | VernacStm (Observe id) -> - return (keyword "Stm Observe " ++ str(Stateid.to_string id)) - | VernacStm (Command v) -> - return (keyword "Stm Command " ++ pr_vernac_body v) - | VernacStm (PGLast v) -> - return (keyword "Stm PGLast " ++ pr_vernac_body v) (* Proof management *) | VernacAbortAll -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8fabb70536..aa422e36af 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -42,8 +42,8 @@ type object_pr = { print_named_decl : Context.Named.Declaration.t -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds; } let gallina_print_module = print_module @@ -71,10 +71,11 @@ let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref = let typ = Global.type_of_global_unsafe ref in + let typ = EConstr.of_constr typ in let typ = if reduce then let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ - in it_mkProd_or_LetIn ccl ctx + in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in let env = Global.env () in @@ -84,7 +85,7 @@ let print_ref reduce ref = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () in - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ Printer.pr_universe_ctx sigma univs) (********************************) @@ -204,6 +205,11 @@ let print_opacity ref = str "transparent (with minimal expansion weight)"] (*******************) + +let print_if_is_coercion ref = + if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] + +(*******************) (* *) let print_polymorphism ref = @@ -257,7 +263,8 @@ let print_name_infos ref = type_info_for_implicit @ print_renames_list (mt()) renames @ print_impargs_list (mt()) impls @ - print_argument_scopes (mt()) scopes + print_argument_scopes (mt()) scopes @ + print_if_is_coercion ref let print_id_args_data test pr id l = if List.exists test l then @@ -432,8 +439,8 @@ let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MOD (**** Gallina layer *****) let gallina_print_typed_value_in_env env sigma (trm,typ) = - (pr_lconstr_env env sigma trm ++ fnl () ++ - str " : " ++ pr_ltype_env env sigma typ) + (pr_leconstr_env env sigma trm ++ fnl () ++ + str " : " ++ pr_letype_env env sigma typ) (* To be improved; the type should be used to provide the types in the abstractions. This should be done recursively inside pr_lconstr, so that @@ -641,6 +648,8 @@ let print_judgment env sigma {uj_val=trm;uj_type=typ} = let print_safe_judgment env sigma j = let trm = Safe_typing.j_val j in let typ = Safe_typing.j_type j in + let trm = EConstr.of_constr trm in + let typ = EConstr.of_constr typ in print_typed_value_in_env env sigma (trm, typ) (*********************) @@ -760,7 +769,9 @@ let print_opaque_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> + let open EConstr in let ty = Universes.unsafe_type_of_global gr in + let ty = EConstr.of_constr ty in print_typed_value (mkConstruct cstr, ty) | VarRef id -> env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 0eab155796..38e1110344 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -27,11 +27,11 @@ val print_full_context_typ : unit -> std_ppcmds val print_full_pure_context : unit -> std_ppcmds val print_sec_context : reference -> std_ppcmds val print_sec_context_typ : reference -> std_ppcmds -val print_judgment : env -> Evd.evar_map -> unsafe_judgment -> std_ppcmds +val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> std_ppcmds val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds val print_eval : reduction_function -> env -> Evd.evar_map -> - Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds + Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds val print_name : reference or_by_notation -> std_ppcmds val print_opaque_name : reference -> std_ppcmds @@ -69,8 +69,8 @@ type object_pr = { print_named_decl : Context.Named.Declaration.t -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; - print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds; + print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds } val set_object_pr : object_pr -> unit diff --git a/printing/printer.ml b/printing/printer.ml index 5e7e9ce548..239e1d7ebe 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -60,7 +60,10 @@ let pr_constr_goal_style_env env = pr_constr_core true env let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c - (* NB do not remove the eta-redexes! Global.env() has side-effects... *) +let pr_leconstr_env env sigma c = pr_lconstr_env env sigma (EConstr.to_constr sigma c) +let pr_econstr_env env sigma c = pr_constr_env env sigma (EConstr.to_constr sigma c) + +(* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = let (sigma, env) = get_current_context () in pr_lconstr_env env sigma t @@ -71,6 +74,9 @@ let pr_constr t = let pr_open_lconstr (_,c) = pr_lconstr c let pr_open_constr (_,c) = pr_constr c +let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c) +let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c) + let pr_constr_under_binders_env_gen pr env sigma (ids,c) = (* Warning: clashes can occur with variables of same name in env but *) (* we also need to preserve the actual names of the patterns *) @@ -78,8 +84,8 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) = let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in pr (Termops.push_rels_assum assums env) sigma c -let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env -let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env +let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env +let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env let pr_constr_under_binders c = let (sigma, env) = get_current_context () in @@ -93,7 +99,6 @@ let pr_type_core goal_concl_style env sigma t = let pr_ltype_core goal_concl_style env sigma t = pr_lconstr_expr (extern_type goal_concl_style env sigma t) -let pr_goal_concl_style_env env = pr_ltype_core true env let pr_ltype_env env = pr_ltype_core false env let pr_type_env env = pr_type_core false env @@ -104,8 +109,13 @@ let pr_type t = let (sigma, env) = get_current_context () in pr_type_env env sigma t +let pr_etype_env env sigma c = pr_type_env env sigma (EConstr.to_constr sigma c) +let pr_letype_env env sigma c = pr_ltype_env env sigma (EConstr.to_constr sigma c) +let pr_goal_concl_style_env env sigma c = + pr_ltype_core true env sigma (EConstr.to_constr sigma c) + let pr_ljudge_env env sigma j = - (pr_lconstr_env env sigma j.uj_val, pr_lconstr_env env sigma j.uj_type) + (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) let pr_ljudge j = let (sigma, env) = get_current_context () in @@ -147,7 +157,7 @@ let pr_constr_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.set_print_constr - (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t)) + (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma (EConstr.Unsafe.to_constr t))) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" @@ -213,7 +223,7 @@ let safe_pr_constr t = let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c + (Univ.pr_universe_context (Termops.pr_evd_level sigma) c)) c else mt() @@ -230,7 +240,7 @@ let pr_puniverses f env (c,u) = else mt ()) let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) -let pr_existential_key = Evd.pr_existential_key +let pr_existential_key = Termops.pr_existential_key let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind) let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr) @@ -496,15 +506,15 @@ let print_evar_constraints gl sigma = | Some g -> let env = Goal.V82.env sigma g in fun e' -> begin - if Context.Named.equal (named_context env) (named_context e') then - if Context.Rel.equal (rel_context env) (rel_context e') then mt () + if Context.Named.equal Constr.equal (named_context env) (named_context e') then + if Context.Rel.equal Constr.equal (rel_context env) (rel_context e') then mt () else pr_rel_context_of e' sigma ++ str " |-" ++ spc () else pr_context_of e' sigma ++ str " |-" ++ spc () end in let pr_evconstr (pbty,env,t1,t2) = - let t1 = Evarutil.nf_evar sigma t1 - and t2 = Evarutil.nf_evar sigma t2 in + let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1) + and t2 = Evarutil.nf_evar sigma (EConstr.of_constr t2) in let env = (** We currently allow evar instances to refer to anonymous de Bruijn indices, so we protect the error printing code in this case by giving @@ -512,13 +522,13 @@ let print_evar_constraints gl sigma = problem. MS: we should rather stop depending on anonymous variables, they can be used to indicate independency. Also, this depends on a strategy for naming/renaming *) - Namegen.make_all_name_different env in + Namegen.make_all_name_different env sigma in str" " ++ - hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++ + hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ pr_lconstr_env env sigma t2) + spc () ++ pr_leconstr_env env sigma t2) in let pr_candidate ev evi (candidates,acc) = if Option.has_some evi.evar_candidates then @@ -767,7 +777,8 @@ let pr_prim_rule = function str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") | Refine c -> - str(if Termops.occur_meta c then "refine " else "exact ") ++ + (** FIXME *) + str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c (* Backwards compatibility *) @@ -918,4 +929,4 @@ let pr_polymorphic b = let pr_universe_instance evd ctx = let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}" + str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" diff --git a/printing/printer.mli b/printing/printer.mli index 20032012a6..504392e35f 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -38,6 +38,13 @@ val safe_pr_lconstr : constr -> std_ppcmds val safe_pr_constr_env : env -> evar_map -> constr -> std_ppcmds val safe_pr_constr : constr -> std_ppcmds +val pr_econstr_env : env -> evar_map -> EConstr.t -> std_ppcmds +val pr_econstr : EConstr.t -> std_ppcmds +val pr_leconstr_env : env -> evar_map -> EConstr.t -> std_ppcmds +val pr_leconstr : EConstr.t -> std_ppcmds + +val pr_etype_env : env -> evar_map -> EConstr.types -> std_ppcmds +val pr_letype_env : env -> evar_map -> EConstr.types -> std_ppcmds val pr_open_constr_env : env -> evar_map -> open_constr -> std_ppcmds val pr_open_constr : open_constr -> std_ppcmds @@ -51,7 +58,7 @@ val pr_constr_under_binders : constr_under_binders -> std_ppcmds val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds -val pr_goal_concl_style_env : env -> evar_map -> types -> std_ppcmds +val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> std_ppcmds val pr_ltype_env : env -> evar_map -> types -> std_ppcmds val pr_ltype : types -> std_ppcmds @@ -61,8 +68,8 @@ val pr_type : types -> std_ppcmds val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> std_ppcmds val pr_closed_glob : closed_glob_constr -> std_ppcmds -val pr_ljudge_env : env -> evar_map -> unsafe_judgment -> std_ppcmds * std_ppcmds -val pr_ljudge : unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge : EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds val pr_lglob_constr_env : env -> glob_constr -> std_ppcmds val pr_lglob_constr : glob_constr -> std_ppcmds diff --git a/printing/printmod.ml b/printing/printmod.ml index baa1b8d791..6f4b162d70 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -94,7 +94,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = Context.Rel.to_extended_list 0 params in + let args = Context.Rel.to_extended_list mkRel 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in @@ -148,7 +148,7 @@ let print_record env mind mib = in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = Context.Rel.to_extended_list 0 params in + let args = Context.Rel.to_extended_list mkRel 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist env cstrtypes.(0) args in |