diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 26202ef4ca..229930142e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -169,12 +169,14 @@ let tag_var = tag Tag.variable let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" let pr_glob_sort = let open Glob_term in function + | GSProp -> tag_type (str "SProp") | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType [] -> tag_type (str "Type") | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) let pr_glob_level = let open Glob_term in function + | GSProp -> tag_type (str "SProp") | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType UUnknown -> tag_type (str "Type") @@ -197,6 +199,8 @@ let tag_var = tag Tag.variable let pr_patvar = pr_id let pr_glob_sort_instance = let open Glob_term in function + | GSProp -> + tag_type (str "SProp") | GProp -> tag_type (str "Prop") | GSet -> @@ -665,10 +669,10 @@ let tag_var = tag Tag.variable (sep() ++ if prec_less prec inherited then strm else surround strm) type term_pr = { - pr_constr_expr : constr_expr -> Pp.t; - pr_lconstr_expr : constr_expr -> Pp.t; - pr_constr_pattern_expr : constr_pattern_expr -> Pp.t; - pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t + pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t; + pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t; + pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t; + pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t } let modular_constr_pr = pr @@ -689,18 +693,16 @@ let tag_var = tag Tag.variable Constrextern.extern_glob_constr (Termops.vars_of_env env) r else c - let pr_expr prec c = - let env = Global.env () in - let sigma = Evd.from_env env in + let pr_expr env sigma prec c = pr prec (transf env sigma c) - let pr_simpleconstr = pr_expr lsimpleconstr + let pr_simpleconstr env sigma = pr_expr env sigma lsimpleconstr let default_term_pr = { pr_constr_expr = pr_simpleconstr; - pr_lconstr_expr = pr_expr ltop; + pr_lconstr_expr = (fun env sigma -> pr_expr env sigma ltop); pr_constr_pattern_expr = pr_simpleconstr; - pr_lconstr_pattern_expr = pr_expr ltop + pr_lconstr_pattern_expr = (fun env sigma -> pr_expr env sigma ltop) } let term_pr = ref default_term_pr @@ -717,5 +719,5 @@ let tag_var = tag Tag.variable let pr_record_body = pr_record_body_gen pr - let pr_binders = pr_undelimited_binders spc (pr_expr ltop) + let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop) |