aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/miscprint.ml25
-rw-r--r--printing/miscprint.mli13
-rw-r--r--printing/ppconstr.ml12
-rw-r--r--printing/ppvernac.ml10
-rw-r--r--printing/prettyp.ml2
-rw-r--r--printing/printer.ml3
6 files changed, 48 insertions, 17 deletions
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 360843711c..a4ecbdf5e5 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -47,3 +47,28 @@ let pr_move_location pr_id = function
| MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
| MoveFirst -> str " at top"
| MoveLast -> str " at bottom"
+
+(** Printing of bindings *)
+let pr_binding prc = function
+ | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
+ | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+let pr_bindings prc prlc = function
+ | ImplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ pr_sequence prc l
+ | ExplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | NoBindings -> mt ()
+
+let pr_bindings_no_with prc prlc = function
+ | ImplicitBindings l ->
+ brk (0,1) ++ prlist_with_sep spc prc l
+ | ExplicitBindings l ->
+ brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | NoBindings -> mt ()
+
+let pr_with_bindings prc prlc (c,bl) =
+ hov 1 (prc c ++ pr_bindings prc prlc bl)
+
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index fe8c779ff4..dbbe3dcfd8 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -22,3 +22,16 @@ val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
val pr_move_location :
('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
+
+val pr_bindings :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+
+val pr_bindings_no_with :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+
+val pr_with_bindings :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds
+
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 60511d9138..49eedb767b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -80,7 +80,7 @@ let tag_var = tag Tag.variable
| Any -> true
let prec_of_prim_token = function
- | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
+ | Numeral (_,b) -> if b then lposint else lnegint
| String _ -> latom
open Notation
@@ -208,7 +208,7 @@ let tag_var = tag Tag.variable
match expl with
| None -> pr (lapp,L) a
| Some (_,ExplByPos (n,_id)) ->
- anomaly (Pp.str "Explicitation by position not implemented")
+ anomaly (Pp.str "Explicitation by position not implemented.")
| Some (_,ExplByName id) ->
str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
@@ -231,7 +231,7 @@ let tag_var = tag Tag.variable
| ArgVar (loc,s) -> pr_lident (loc,s)
let pr_prim_token = function
- | Numeral n -> str (Bigint.to_string n)
+ | Numeral (n,s) -> str (if s then n else "-"^n)
| String s -> qs s
let pr_evar pr id l =
@@ -423,7 +423,7 @@ let tag_var = tag Tag.variable
| CLambdaN ([[na],bk,t],c) -> (na,t,c)
| CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c))
| CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c))
- | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+ | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
)
let rename na na' t c =
@@ -438,7 +438,7 @@ let tag_var = tag Tag.variable
| CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c))
| CProdN ((na::nal,bk,t)::bl,c) ->
rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c))
- | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+ | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
)
let rec split_fix n typ def =
@@ -485,7 +485,7 @@ let tag_var = tag Tag.variable
pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
let pr_recursive pr_decl id = function
- | [] -> anomaly (Pp.str "(co)fixpoint with no definition")
+ | [] -> anomaly (Pp.str "(co)fixpoint with no definition.")
| [d1] -> pr_decl false d1
| dl ->
prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ())
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 6aa136b606..9d28bc4f84 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -118,7 +118,7 @@ open Decl_kinds
let pr_explanation (e,b,f) =
let a = match e with
- | ExplByPos (n,_) -> anomaly (Pp.str "No more supported")
+ | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.")
| ExplByName id -> pr_id id in
let a = if f then str"!" ++ a else a in
if b then str "[" ++ a ++ str "]" else a
@@ -318,7 +318,7 @@ open Decl_kinds
keyword (if many then "Local Parameters" else "Local Parameter")
| (Global,Conjectural) -> str"Conjecture"
| ((Discharge | Local),Conjectural) ->
- anomaly (Pp.str "Don't know how to beautify a local conjecture")
+ anomaly (Pp.str "Don't know how to beautify a local conjecture.")
let pr_params pr_c (xl,(c,t)) =
hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
@@ -561,17 +561,13 @@ open Decl_kinds
| GoalUid n -> spc () ++ str n in
let pr_showable = function
| ShowGoal n -> keyword "Show" ++ pr_goal_reference n
- | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n
| ShowProof -> keyword "Show Proof"
- | ShowNode -> keyword "Show Node"
| ShowScript -> keyword "Show Script"
| ShowExistentials -> keyword "Show Existentials"
| ShowUniverses -> keyword "Show Universes"
- | ShowTree -> keyword "Show Tree"
| ShowProofNames -> keyword "Show Conjectures"
| ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
| ShowMatch id -> keyword "Show Match " ++ pr_reference id
- | ShowThesis -> keyword "Show Thesis"
in
return (pr_showable s)
| VernacCheckGuard ->
@@ -1075,7 +1071,7 @@ open Decl_kinds
)
| VernacSetOpacity _ ->
return (
- CErrors.anomaly (keyword "VernacSetOpacity used to set something else")
+ CErrors.anomaly (keyword "VernacSetOpacity used to set something else.")
)
| VernacSetStrategy l ->
let pr_lev = function
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2b21b3f9e8..3ae7da8fc1 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -587,8 +587,6 @@ let gallina_print_library_entry with_values ent =
Some (str " >>>>>>> Module " ++ pr_name oname)
| (oname,Lib.ClosedModule _) ->
Some (str " >>>>>>> Closed Module " ++ pr_name oname)
- | (_,Lib.FrozenState _) ->
- None
let gallina_print_context with_values =
let rec prec n = function
diff --git a/printing/printer.ml b/printing/printer.ml
index 3c31dd96bf..d6f0778f75 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -17,7 +17,6 @@ open Nametab
open Evd
open Proof_type
open Refiner
-open Pfedit
open Constrextern
open Ppconstr
open Declarations
@@ -812,7 +811,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
end
let pr_nth_open_subgoal n =
- let pf = get_pftreestate () in
+ let pf = Proof_global.give_me_the_proof () in
let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
pr_subgoal n sigma gls
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 05:39:23 +0000