aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml60
-rw-r--r--printing/ppconstr.mli1
-rw-r--r--printing/prettyp.ml15
-rw-r--r--printing/proof_diffs.ml2
4 files changed, 39 insertions, 39 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 78733784a7..27ed2189ed 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -157,10 +157,14 @@ let tag_var = tag Tag.variable
let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
- let pr_univ_expr = function
- | Some (x,n) ->
- pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
- | None -> str"_"
+ let pr_glob_sort_name = function
+ | GSProp -> str "SProp"
+ | GProp -> str "Prop"
+ | GSet -> str "Set"
+ | GType qid -> pr_qualid qid
+
+ let pr_univ_expr (u,n) =
+ pr_glob_sort_name u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
let pr_univ l =
match l with
@@ -170,19 +174,20 @@ 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)
+ | UNamed [GSProp,0] -> tag_type (str "SProp")
+ | UNamed [GProp,0] -> tag_type (str "Prop")
+ | UNamed [GSet,0] -> tag_type (str "Set")
+ | UAnonymous {rigid=true} -> tag_type (str "Type")
+ | UAnonymous {rigid=false} -> tag_type (str "Type") ++ pr_univ_annot (fun _ -> str "_") ()
+ | UNamed 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")
- | GType UAnonymous -> tag_type (str "_")
- | GType (UNamed u) -> tag_type (pr_qualid u)
+ | UNamed GSProp -> tag_type (str "SProp")
+ | UNamed GProp -> tag_type (str "Prop")
+ | UNamed GSet -> tag_type (str "Set")
+ | UAnonymous {rigid=true} -> tag_type (str "Type")
+ | UAnonymous {rigid=false} -> tag_type (str "_")
+ | UNamed (GType u) -> tag_type (pr_qualid u)
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
@@ -199,21 +204,8 @@ let tag_var = tag Tag.variable
let pr_qualid = pr_qualid
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 ->
- tag_type (str "Set")
- | GType u ->
- (match u with
- | UNamed u -> pr_qualid u
- | UAnonymous -> tag_type (str "Type")
- | UUnknown -> tag_type (str "_"))
-
let pr_universe_instance l =
- pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
+ pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_level)) l
let pr_reference qid =
if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid)
@@ -249,7 +241,7 @@ let tag_var = tag Tag.variable
str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}"))
let las = lapp
- let lpator = 100
+ let lpator = 0
let lpatrec = 0
let rec pr_patt sep inh p =
@@ -283,7 +275,8 @@ let tag_var = tag Tag.variable
pr_reference r, latom
| CPatOr pl ->
- hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator
+ let pp = pr_patt mt (lpator,Any) in
+ surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator
| CPatNotation ((_,"( _ )"),([p],[]),[]) ->
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
@@ -339,8 +332,7 @@ let tag_var = tag Tag.variable
let pr_binder many pr (nal,k,t) =
match k with
- | Generalized (b, b', t') ->
- assert (match b with Implicit -> true | _ -> false);
+ | Generalized (b', t') ->
begin match nal with
|[{loc; v=Anonymous}] ->
hov 1 (str"`" ++ (surround_impl b'
@@ -349,7 +341,7 @@ let tag_var = tag Tag.variable
hov 1 (str "`" ++ (surround_impl b'
(pr_lident CAst.(make ?loc id) ++ str " : " ++
(if t' then str "!" else mt()) ++ pr t)))
- |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.")
+ |_ -> anomaly (Pp.str "List of generalized binders have always one element.")
end
| Default b ->
match t with
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 1332cd0168..219fe4336a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -33,6 +33,7 @@ val pr_id : Id.t -> Pp.t
val pr_qualid : qualid -> Pp.t
val pr_patvar : Pattern.patvar -> Pp.t
+val pr_glob_sort_name : Glob_term.glob_sort_name -> Pp.t
val pr_glob_level : Glob_term.glob_level -> Pp.t
val pr_glob_sort : Glob_term.glob_sort -> Pp.t
val pr_guard_annot
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 9541ea5882..f55bfb504f 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -304,6 +304,12 @@ let print_inductive_argument_scopes =
print_args_data_of_inductive_ids
Notation.find_arguments_scope (Option.has_some) print_argument_scopes
+let print_bidi_hints gr =
+ match Pretyping.get_bidirectionality_hint gr with
+ | None -> []
+ | Some nargs ->
+ [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"]
+
(*********************)
(* "Locate" commands *)
@@ -549,7 +555,7 @@ let print_instance sigma cb =
let print_constant with_values sep sp udecl =
let cb = Global.lookup_constant sp in
- let val_0 = Global.body_of_constant_body cb in
+ let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in
let typ = cb.const_type in
let univs =
let open Univ in
@@ -557,7 +563,7 @@ let print_constant with_values sep sp udecl =
match cb.const_body with
| Undef _ | Def _ | Primitive _ -> cb.const_universes
| OpaqueDef o ->
- let body_uctxs = Opaqueproof.force_constraints otab o in
+ let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in
match cb.const_universes with
| Monomorphic ctx ->
Monomorphic (ContextSet.union body_uctxs ctx)
@@ -717,7 +723,7 @@ let print_full_pure_context env sigma =
| OpaqueDef lc ->
str "Theorem " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
- str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof (Global.opaque_tables ()) lc)
+ str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc)
| Def c ->
str "Definition " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
@@ -841,7 +847,8 @@ let print_about_any ?loc env sigma k udecl =
print_name_infos ref @
(if Pp.ismt rb then [] else [rb]) @
print_opacity ref @
- [hov 0 (str "Expands to: " ++ pr_located_qualid k)])
+ print_bidi_hints ref @
+ [hov 0 (str "Expands to: " ++ pr_located_qualid k)])
| Syntactic kn ->
let () = match Syntax_def.search_syntactic_definition kn with
| [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index f378a5d2dd..abb0d55b39 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -408,7 +408,7 @@ the call to db_goal_map and entering the following:
let match_goals ot nt =
let nevar_to_oevar = ref StringMap.empty in
(* ogname is "" when there is no difference on the current path.
- It's set to the old goal's evar name once a rewitten goal is found,
+ It's set to the old goal's evar name once a rewritten goal is found,
at which point the code only searches for the replacing goals
(and ot is set to nt). *)
let iter2 f l1 l2 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 23:48:37 +0000