aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml13
-rw-r--r--printing/genprint.mli2
-rw-r--r--printing/miscprint.ml6
-rw-r--r--printing/miscprint.mli2
-rw-r--r--printing/ppannotation.ml4
-rw-r--r--printing/ppannotation.mli3
-rw-r--r--printing/ppconstr.ml56
-rw-r--r--printing/ppconstr.mli2
-rw-r--r--printing/ppconstrsig.mli2
-rw-r--r--printing/pptactic.ml1021
-rw-r--r--printing/pptactic.mli15
-rw-r--r--printing/pptacticsig.mli70
-rw-r--r--printing/pputils.ml2
-rw-r--r--printing/pputils.mli2
-rw-r--r--printing/ppvernac.ml178
-rw-r--r--printing/ppvernac.mli2
-rw-r--r--printing/ppvernacsig.mli2
-rw-r--r--printing/prettyp.ml85
-rw-r--r--printing/prettyp.mli4
-rw-r--r--printing/printer.ml191
-rw-r--r--printing/printer.mli39
-rw-r--r--printing/printing.mllib4
-rw-r--r--printing/printmod.ml67
-rw-r--r--printing/printmod.mli2
-rw-r--r--printing/printmodsig.mli2
-rw-r--r--printing/richprinter.ml25
-rw-r--r--printing/richprinter.mli39
27 files changed, 867 insertions, 973 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index ade69ef831..0ec35e07be 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -19,8 +19,9 @@ module PrintObj =
struct
type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer
let name = "printer"
- let default wit = match unquote (rawwit wit) with
- | ExtraArgType name ->
+ let default wit = match wit with
+ | ExtraArg tag ->
+ let name = ArgT.repr tag in
let printer = {
raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
@@ -40,6 +41,6 @@ let raw_print wit v = (Print.obj wit).raw v
let glb_print wit v = (Print.obj wit).glb v
let top_print wit v = (Print.obj wit).top v
-let generic_raw_print v = unpack { unpacker = fun w v -> raw_print w (raw v); } v
-let generic_glb_print v = unpack { unpacker = fun w v -> glb_print w (glb v); } v
-let generic_top_print v = unpack { unpacker = fun w v -> top_print w (top v); } v
+let generic_raw_print (GenArg (Rawwit w, v)) = raw_print w v
+let generic_glb_print (GenArg (Glbwit w, v)) = glb_print w v
+let generic_top_print (GenArg (Topwit w, v)) = top_print w v
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 5b91d6d216..6e6626f2f6 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index d09af6d2ac..5e86c6bd76 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -33,9 +33,9 @@ and pr_intro_pattern_action prc = function
| IntroRewrite false -> str "<-"
and pr_or_and_intro_pattern prc = function
- | [pl] ->
+ | IntroAndPattern pl ->
str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
- | pll ->
+ | IntroOrPattern pll ->
str "[" ++
hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
++ str "]"
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index 1d915ef8c5..fe8c779ff4 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index 4f26b82424..511f93569c 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -20,7 +20,6 @@ type t =
| AGlobAtomicTacticExpr of glob_atomic_tactic_expr
| ARawTacticExpr of raw_tactic_expr
| ARawAtomicTacticExpr of raw_atomic_tactic_expr
- | ATacticExpr of tactic_expr
| AAtomicTacticExpr of atomic_tactic_expr
let tag_of_annotation = function
@@ -32,7 +31,6 @@ let tag_of_annotation = function
| AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr"
| ARawTacticExpr _ -> "raw_tactic_expr"
| ARawAtomicTacticExpr _ -> "raw_atomic_tactic_expr"
- | ATacticExpr _ -> "tactic_expr"
| AAtomicTacticExpr _ -> "atomic_tactic_expr"
let attributes_of_annotation a =
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index bc345c347b..a0fef1a757 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -23,7 +23,6 @@ type t =
| AGlobAtomicTacticExpr of glob_atomic_tactic_expr
| ARawTacticExpr of raw_tactic_expr
| ARawAtomicTacticExpr of raw_atomic_tactic_expr
- | ATacticExpr of tactic_expr
| AAtomicTacticExpr of atomic_tactic_expr
val tag_of_annotation : t -> string
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 650b8f7262..1866ca5042 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -136,12 +136,10 @@ end) = struct
let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
- let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
-
let pr_univ l =
match l with
- | [x] -> str x
- | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")"
+ | [_,x] -> str x
+ | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")"
let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
@@ -153,11 +151,11 @@ end) = struct
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
- let id = tag_ref (str (Id.to_string id)) in
+ let id = tag_ref (pr_id id) in
let sl = match List.rev (DirPath.repr sl) with
| [] -> mt ()
| sl ->
- let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in
+ let pr dir = tag_path (pr_id dir) ++ str "." in
prlist pr sl
in
sl ++ id
@@ -174,7 +172,7 @@ end) = struct
tag_type (str "Set")
| GType u ->
(match u with
- | Some u -> str u
+ | Some (_,u) -> str u
| None -> tag_type (str "Type"))
let pr_universe_instance l =
@@ -182,7 +180,7 @@ end) = struct
let pr_reference = function
| Qualid (_, qid) -> pr_qualid qid
- | Ident (_, id) -> tag_var (str (Id.to_string id))
+ | Ident (_, id) -> tag_var (pr_id id)
let pr_cref ref us =
pr_reference ref ++ pr_universe_instance us
@@ -246,16 +244,16 @@ end) = struct
| CPatAlias (_, p, id) ->
pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
- | CPatCstr (_,c, [], []) ->
+ | CPatCstr (_,c, None, []) ->
pr_reference c, latom
- | CPatCstr (_, c, [], args) ->
+ | CPatCstr (_, c, None, args) ->
pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
- | CPatCstr (_, c, args, []) ->
+ | CPatCstr (_, c, Some args, []) ->
str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
- | CPatCstr (_, c, expl_args, extra_args) ->
+ | CPatCstr (_, c, Some expl_args, extra_args) ->
surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args)
++ prlist (pr_patt spc (lapp,L)) extra_args, lapp
@@ -457,7 +455,7 @@ end) = struct
(pr_decl true) dl ++
fnl() ++ keyword "for" ++ spc () ++ pr_id id
- let pr_asin pr (na,indnalopt) =
+ let pr_asin pr na indnalopt =
(match na with (* Decision of printing "_" or not moved to constrextern.ml *)
| Some na -> spc () ++ keyword "as" ++ spc () ++ pr_lname na
| None -> mt ()) ++
@@ -465,8 +463,8 @@ end) = struct
| None -> mt ()
| Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t)
- let pr_case_item pr (tm,asin) =
- hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
+ let pr_case_item pr (tm,as_clause, in_clause) =
+ hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause)
let pr_case_type pr po =
match po with
@@ -595,28 +593,20 @@ end) = struct
return (p, lproj)
| CApp (_,(None,a),l) ->
return (pr_app (pr mt) a l, lapp)
- | CRecord (_,w,l) ->
- let beg =
- match w with
- | None ->
- spc ()
- | Some t ->
- spc () ++ pr spc ltop t ++ spc ()
- ++ keyword "with" ++ spc ()
- in
+ | CRecord (_,l) ->
return (
- hv 0 (str"{|" ++ beg ++
+ hv 0 (str"{|" ++ spc () ++
prlist_with_sep pr_semicolon
(fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l
++ str" |}"),
latom
)
- | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
+ | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) ->
return (
hv 0 (
keyword "let" ++ spc () ++ str"'" ++
hov 0 (pr_patt ltop p ++
- pr_asin (pr_dangling_with_for mt pr) asin ++
+ pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++
str " :=" ++ pr spc ltop c ++
pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
spc () ++ keyword "in" ++ pr spc ltop b)),
@@ -638,13 +628,13 @@ end) = struct
| CLetTuple (_,nal,(na,po),c,b) ->
return (
hv 0 (
- keyword "let" ++ spc () ++
- hov 0 (str "(" ++
+ hov 2 (keyword "let" ++ spc () ++
+ hov 1 (str "(" ++
prlist_with_sep sep_v pr_lname nal ++
str ")" ++
- pr_simple_return_type (pr mt) na po ++ str " :=" ++
- pr spc ltop c ++ spc ()
- ++ keyword "in") ++
+ pr_simple_return_type (pr mt) na po ++ str " :=") ++
+ pr spc ltop c
+ ++ keyword " in") ++
pr spc ltop b),
lletin
)
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 6e8d3b04c4..0241633c61 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index b7eb9b1fff..c711dd8f7f 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index b8ad996aa3..5356cdee8a 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -14,6 +14,7 @@ open Util
open Constrexpr
open Tacexpr
open Genarg
+open Geninterp
open Constrarg
open Libnames
open Ppextend
@@ -26,23 +27,20 @@ open Printer
let pr_global x = Nametab.pr_global_env Id.Set.empty x
-type grammar_terminals = string option list
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
+
+type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
type pp_tactic = {
- pptac_args : argument_type list;
- pptac_prods : int * grammar_terminals;
+ pptac_level : int;
+ pptac_prods : grammar_terminals;
}
-(* ML Extensions *)
-let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t =
- Hashtbl.create 17
-
(* Tactic notations *)
let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
-let declare_ml_tactic_pprule key pt =
- Hashtbl.add prtac_tab key pt
-
let declare_notation_tactic_pprule kn pt =
prnotation_tab := KNmap.add kn pt !prnotation_tab
@@ -61,14 +59,14 @@ type 'a glob_extra_genarg_printer =
type 'a extra_genarg_printer =
(Term.constr -> std_ppcmds) ->
(Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ (tolerability -> Val.t -> std_ppcmds) ->
'a -> std_ppcmds
let genarg_pprule = ref String.Map.empty
let declare_extra_genarg_pprule wit f g h =
- let s = match unquote (topwit wit) with
- | ExtraArgType s -> s
+ let s = match wit with
+ | ExtraArg s -> ArgT.repr s
| _ -> error
"Can declare a pretty-printing rule only for extra argument types."
in
@@ -94,8 +92,6 @@ module Make
: raw_tactic_expr -> std_ppcmds -> std_ppcmds
val tag_raw_atomic_tactic_expr
: raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_tactic_expr
- : tactic_expr -> std_ppcmds -> std_ppcmds
val tag_atomic_tactic_expr
: atomic_tactic_expr -> std_ppcmds -> std_ppcmds
end)
@@ -106,6 +102,39 @@ module Make
let keyword x = tag_keyword (str x)
let primitive x = tag_primitive (str x)
+ let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with
+ | None -> false
+ | Some _ -> true
+
+ let unbox : type a. Val.t -> a Val.typ -> a= fun (Val.Dyn (tag, x)) t ->
+ match Val.eq tag t with
+ | None -> assert false
+ | Some Refl -> x
+
+ let rec pr_value lev v : std_ppcmds =
+ if has_type v Val.typ_list then
+ pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list)
+ else if has_type v Val.typ_opt then
+ pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt)
+ else if has_type v Val.typ_pair then
+ let (v1, v2) = unbox v Val.typ_pair in
+ str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")"
+ else
+ let Val.Dyn (tag, x) = v in
+ let name = Val.repr tag in
+ let default = str "<" ++ str name ++ str ">" in
+ match ArgT.name name with
+ | None -> default
+ | Some (ArgT.Any arg) ->
+ let wit = ExtraArg arg in
+ match val_tag (Topwit wit) with
+ | Val.Base t ->
+ begin match Val.eq t tag with
+ | None -> default
+ | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+ end
+ | _ -> default
+
let pr_with_occurrences pr (occs,c) =
match occs with
| AllOccurrences ->
@@ -264,165 +293,69 @@ module Make
let with_evars ev s = if ev then "e" ^ s else s
+ let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
- let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
- match Genarg.genarg_tag x with
- | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
- | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
- | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
- | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
- | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
- | ConstrMayEvalArgType ->
- pr_may_eval prc prlc (pr_or_by_notation prref) prpat
- (out_gen (rawwit wit_constr_may_eval) x)
- | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x)
- | RedExprArgType ->
- pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
- (out_gen (rawwit wit_red_expr) x)
- | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
- | ConstrWithBindingsArgType ->
- pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
- | BindingsArgType ->
- pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
- | ListArgType _ ->
- let list_unpacker wit l =
- let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
- pr_sequence map (raw l)
- in
- hov 0 (list_unpack { list_unpacker } x)
- | OptArgType _ ->
- let opt_unpacker wit o = match raw o with
+ let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) =
+ match wit with
+ | ListArg wit ->
+ let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
+ let ans = pr_sequence map x in
+ hov_if_not_empty 0 ans
+ | OptArg wit ->
+ let ans = match x with
| None -> mt ()
- | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x)
- in
- hov 0 (opt_unpack { opt_unpacker } x)
- | PairArgType _ ->
- let pair_unpacker wit1 wit2 o =
- let p, q = raw o in
- let p = in_gen (rawwit wit1) p in
- let q = in_gen (rawwit wit2) q in
- pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q]
- in
- hov 0 (pair_unpack { pair_unpacker } x)
- | ExtraArgType s ->
- try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> Genprint.generic_raw_print x
-
-
- let rec pr_glb_generic prc prlc prtac prpat x =
- match Genarg.genarg_tag x with
- | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
- | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
- | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
- | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
- | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
- | ConstrMayEvalArgType ->
- pr_may_eval prc prlc
- (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
- (out_gen (glbwit wit_constr_may_eval) x)
- | QuantHypArgType ->
- pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x)
- | RedExprArgType ->
- pr_red_expr
- (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
- (out_gen (glbwit wit_red_expr) x)
- | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
- | ConstrWithBindingsArgType ->
- pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
- | BindingsArgType ->
- pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
- | ListArgType _ ->
- let list_unpacker wit l =
- let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in
- pr_sequence map (glb l)
- in
- hov 0 (list_unpack { list_unpacker } x)
- | OptArgType _ ->
- let opt_unpacker wit o = match glb o with
- | None -> mt ()
- | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
- in
- hov 0 (opt_unpack { opt_unpacker } x)
- | PairArgType _ ->
- let pair_unpacker wit1 wit2 o =
- let p, q = glb o in
- let p = in_gen (glbwit wit1) p in
- let q = in_gen (glbwit wit2) q in
- pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q]
- in
- hov 0 (pair_unpack { pair_unpacker } x)
- | ExtraArgType s ->
- try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> Genprint.generic_glb_print x
-
- let rec pr_top_generic prc prlc prtac prpat x =
- match Genarg.genarg_tag x with
- | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
- | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
- | VarArgType -> pr_id (out_gen (topwit wit_var) x)
- | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
- | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
- | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
- | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x)
- | RedExprArgType ->
- pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
- (out_gen (topwit wit_red_expr) x)
- | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
- | ConstrWithBindingsArgType ->
- let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
- pr_with_bindings prc prlc (c,b)
- | BindingsArgType ->
- pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
- | ListArgType _ ->
- let list_unpacker wit l =
- let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in
- pr_sequence map (top l)
+ | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x)
in
- hov 0 (list_unpack { list_unpacker } x)
- | OptArgType _ ->
- let opt_unpacker wit o = match top o with
+ hov_if_not_empty 0 ans
+ | PairArg (wit1, wit2) ->
+ let p, q = x in
+ let p = in_gen (rawwit wit1) p in
+ let q = in_gen (rawwit wit2) q in
+ hov_if_not_empty 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q])
+ | ExtraArg s ->
+ try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x)
+ with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x)
+
+
+ let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) =
+ match wit with
+ | ListArg wit ->
+ let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
+ let ans = pr_sequence map x in
+ hov_if_not_empty 0 ans
+ | OptArg wit ->
+ let ans = match x with
| None -> mt ()
- | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x)
+ | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
in
- hov 0 (opt_unpack { opt_unpacker } x)
- | PairArgType _ ->
- let pair_unpacker wit1 wit2 o =
- let p, q = top o in
- let p = in_gen (topwit wit1) p in
- let q = in_gen (topwit wit2) q in
- pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q]
- in
- hov 0 (pair_unpack { pair_unpacker } x)
- | ExtraArgType s ->
- try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> Genprint.generic_top_print x
+ hov_if_not_empty 0 ans
+ | PairArg (wit1, wit2) ->
+ let p, q = x in
+ let p = in_gen (glbwit wit1) p in
+ let q = in_gen (glbwit wit2) q in
+ let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in
+ hov_if_not_empty 0 ans
+ | ExtraArg s ->
+ try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x)
+ with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x)
let rec tacarg_using_rule_token pr_gen = function
- | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
- | None :: l, a :: al ->
- let r = tacarg_using_rule_token pr_gen (l,al) in
- pr_gen a :: r
- | [], [] -> []
- | _ -> failwith "Inconsistent arguments of extended tactic"
+ | [] -> []
+ | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l
+ | TacNonTerm (_, (symb, arg), _) :: l ->
+ pr_gen symb arg :: tacarg_using_rule_token pr_gen l
let pr_tacarg_using_rule pr_gen l =
let l = match l with
- | (Some s :: l, al) ->
+ | TacTerm s :: l ->
(** First terminal token should be considered as the name of the tactic,
so we tag it differently than the other terminal tokens. *)
- primitive s :: (tacarg_using_rule_token pr_gen (l, al))
+ primitive s :: tacarg_using_rule_token pr_gen l
| _ -> tacarg_using_rule_token pr_gen l
in
pr_sequence (fun x -> x) l
let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
- try
- let pp_rules = Hashtbl.find prtac_tab s in
- let pp = pp_rules.(i) in
- let (lev', pl) = pp.pptac_prods in
- let p = pr_tacarg_using_rule pr_gen (pl,l) in
- if lev' > lev then surround p else p
- with Not_found ->
let name =
str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
str "@" ++ int i
@@ -433,28 +366,99 @@ module Make
in
str "<" ++ name ++ str ">" ++ args
+ let pr_alias_key key =
+ try
+ let prods = (KNmap.find key !prnotation_tab).pptac_prods in
+ (* First printing strategy: only the head symbol *)
+ match prods with
+ | TacTerm s :: prods -> str s
+ | _ ->
+ (* Second printing strategy; if ever Tactic Notation is eventually *)
+ (* accepting notations not starting with an identifier *)
+ let rec pr = function
+ | [] -> []
+ | TacTerm s :: prods -> s :: pr prods
+ | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in
+ str (String.concat " " (pr prods))
+ with Not_found ->
+ KerName.print key
+
let pr_alias_gen pr_gen lev key l =
try
let pp = KNmap.find key !prnotation_tab in
- let (lev', pl) = pp.pptac_prods in
- let p = pr_tacarg_using_rule pr_gen (pl, l) in
- if lev' > lev then surround p else p
+ let rec pack prods args = match prods, args with
+ | [], [] -> []
+ | TacTerm s :: prods, args -> TacTerm s :: pack prods args
+ | TacNonTerm (loc, symb, id) :: prods, arg :: args ->
+ TacNonTerm (loc, (symb, arg), id) :: pack prods args
+ | _ -> raise Not_found
+ in
+ let prods = pack pp.pptac_prods l in
+ let p = pr_tacarg_using_rule pr_gen prods in
+ if pp.pptac_level > lev then surround p else p
with Not_found ->
- KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
-
- let pr_raw_extend prc prlc prtac prpat =
- pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
- let pr_glob_extend prc prlc prtac prpat =
- pr_extend_gen (pr_glb_generic prc prlc prtac prpat)
- let pr_extend prc prlc prtac prpat =
- pr_extend_gen (pr_top_generic prc prlc prtac prpat)
-
- let pr_raw_alias prc prlc prtac prpat =
- pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
- let pr_glob_alias prc prlc prtac prpat =
- pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
- let pr_alias prc prlc prtac prpat =
- pr_alias_gen (pr_top_generic prc prlc prtac prpat)
+ let pr arg = str "_" in
+ KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
+
+ let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg))
+
+ let is_genarg tag wit =
+ let ArgT.Any tag = tag in
+ argument_type_eq (ArgumentType (ExtraArg tag)) wit
+
+ let get_list : type l. l generic_argument -> l generic_argument list option =
+ function (GenArg (wit, arg)) -> match wit with
+ | Rawwit (ListArg wit) -> Some (List.map (in_gen (rawwit wit)) arg)
+ | Glbwit (ListArg wit) -> Some (List.map (in_gen (glbwit wit)) arg)
+ | _ -> None
+
+ let get_opt : type l. l generic_argument -> l generic_argument option option =
+ function (GenArg (wit, arg)) -> match wit with
+ | Rawwit (OptArg wit) -> Some (Option.map (in_gen (rawwit wit)) arg)
+ | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg)
+ | _ -> None
+
+ let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds =
+ fun prtac symb arg -> match symb with
+ | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg
+ | Extend.Ulist1 s | Extend.Ulist0 s ->
+ begin match get_list arg with
+ | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | Some l -> pr_sequence (pr_any_arg prtac s) l
+ end
+ | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) ->
+ begin match get_list arg with
+ | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l
+ end
+ | Extend.Uopt s ->
+ begin match get_opt arg with
+ | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | Some l -> pr_opt (pr_any_arg prtac s) l
+ end
+ | Extend.Uentry _ | Extend.Uentryl _ ->
+ str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+
+ let rec pr_targ prtac symb arg = match symb with
+ | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
+ prtac (1, Any) arg
+ | Extend.Uentryl (_, l) -> prtac (l, Any) arg
+ | _ ->
+ match arg with
+ | TacGeneric arg ->
+ let pr l arg = prtac l (TacGeneric arg) in
+ pr_any_arg pr symb arg
+ | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+
+ let pr_raw_extend_rec prc prlc prtac prpat =
+ pr_extend_gen (pr_farg prtac)
+ let pr_glob_extend_rec prc prlc prtac prpat =
+ pr_extend_gen (pr_farg prtac)
+
+ let pr_raw_alias prc prlc prtac prpat lev key args =
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
+ let pr_glob_alias prc prlc prtac prpat lev key args =
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
(**********************************************************************)
(* The tactic printer *)
@@ -563,9 +567,8 @@ module Make
| ipat ->
spc() ++ prc c ++ pr_as_ipat prdc ipat
- let pr_by_tactic prt = function
- | TacId [] -> mt ()
- | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac
+ let pr_by_tactic prt tac =
+ spc() ++ keyword "by" ++ spc () ++ prt tac
let pr_hyp_location pr_id = function
| occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
@@ -578,7 +581,7 @@ module Make
str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
) occs
- let pr_in pp = spc () ++ hov 0 (keyword "in" ++ pp)
+ let pr_in pp = hov 0 (keyword "in" ++ pp)
let pr_simple_hyp_clause pr_id = function
| [] -> mt ()
@@ -586,8 +589,7 @@ module Make
let pr_in_hyp_as prc pr_id = function
| None -> mt ()
- | Some (clear,id,ipat) ->
- pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat
+ | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
let pr_clauses default_is_concl pr_id = function
| { onhyps=Some []; concl_occs=occs }
@@ -712,20 +714,13 @@ module Make
str " ]")
let pr_hintbases = function
- | None -> spc () ++ keyword "with" ++ str" *"
+ | None -> keyword "with" ++ str" *"
| Some [] -> mt ()
- | Some l ->
- spc () ++ hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
+ | Some l -> hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
let pr_auto_using prc = function
| [] -> mt ()
- | l -> spc () ++
- hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
-
- let string_of_debug = function
- | Off -> ""
- | Debug -> "debug "
- | Info -> "info_"
+ | l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
let pr_then () = str ";"
@@ -752,7 +747,6 @@ module Make
type 'a printer = {
pr_tactic : tolerability -> 'tacexpr -> std_ppcmds;
pr_constr : 'trm -> std_ppcmds;
- pr_uconstr : 'utrm -> std_ppcmds;
pr_lconstr : 'trm -> std_ppcmds;
pr_dconstr : 'dtrm -> std_ppcmds;
pr_pattern : 'pat -> std_ppcmds;
@@ -761,13 +755,12 @@ module Make
pr_reference : 'ref -> std_ppcmds;
pr_name : 'nam -> std_ppcmds;
pr_generic : 'lev generic_argument -> std_ppcmds;
- pr_extend : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds;
- pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
+ pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds;
+ pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds;
}
constraint 'a = <
term :'trm;
- utrm :'utrm;
dterm :'dtrm;
pattern :'pat;
constant :'cst;
@@ -777,306 +770,219 @@ module Make
level :'lev
>
- let make_pr_tac pr strip_prod_binders tag_atom tag =
-
- (* some shortcuts *)
- let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
- let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in
- let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
- let pr_with_bindings_arg_full = pr_with_bindings_arg in
- let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
- let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
-
- let pr_constrarg c = spc () ++ pr.pr_constr c in
- let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
- let pr_intarg n = spc () ++ int n in
-
- (* Some printing combinators *)
- let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
-
- let extract_binders = function
- | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
- | body -> ([],body) in
-
- let pr_binder_fix (nal,t) =
- (* match t with
- | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
- | _ ->*)
- let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
- spc() ++ hov 1 (str"(" ++ s ++ str")") in
-
- let pr_fix_tac (id,n,c) =
- let rec set_nth_name avoid n = function
- (nal,ty)::bll ->
- if n <= List.length nal then
- match List.chop (n-1) nal with
- _, (_,Name id) :: _ -> id, (nal,ty)::bll
- | bef, (loc,Anonymous) :: aft ->
- let id = next_ident_away (Id.of_string"y") avoid in
- id, ((bef@(loc,Name id)::aft, ty)::bll)
- | _ -> assert false
- else
- let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
- (id,(nal,ty)::bll')
- | [] -> assert false in
- let (bll,ty) = strip_prod_binders n c in
- let names =
- List.fold_left
- (fun ln (nal,_) -> List.fold_left
- (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
- ln nal)
- [] bll in
- let idarg,bll = set_nth_name names n bll in
- let annot = match names with
- | [_] ->
- mt ()
- | _ ->
- spc() ++ str"{"
- ++ keyword "struct" ++ spc ()
- ++ pr_id idarg ++ str"}"
- in
- hov 1 (str"(" ++ pr_id id ++
- prlist pr_binder_fix bll ++ annot ++ str" :" ++
- pr_lconstrarg ty ++ str")") in
- (* spc() ++
- hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
- c)
+ let pr_atom pr strip_prod_binders tag_atom =
+ let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
+ let pr_with_bindings_arg_full = pr_with_bindings_arg in
+ let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
+ let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
+
+ let pr_constrarg c = spc () ++ pr.pr_constr c in
+ let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
+ let pr_intarg n = spc () ++ int n in
+
+ (* Some printing combinators *)
+ let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
+
+ let pr_binder_fix (nal,t) =
+ (* match t with
+ | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
+ | _ ->*)
+ let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+ spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+ let pr_fix_tac (id,n,c) =
+ let rec set_nth_name avoid n = function
+ (nal,ty)::bll ->
+ if n <= List.length nal then
+ match List.chop (n-1) nal with
+ _, (_,Name id) :: _ -> id, (nal,ty)::bll
+ | bef, (loc,Anonymous) :: aft ->
+ let id = next_ident_away (Id.of_string"y") avoid in
+ id, ((bef@(loc,Name id)::aft, ty)::bll)
+ | _ -> assert false
+ else
+ let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+ (id,(nal,ty)::bll')
+ | [] -> assert false in
+ let (bll,ty) = strip_prod_binders n c in
+ let names =
+ List.fold_left
+ (fun ln (nal,_) -> List.fold_left
+ (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+ ln nal)
+ [] bll in
+ let idarg,bll = set_nth_name names n bll in
+ let annot = match names with
+ | [_] ->
+ mt ()
+ | _ ->
+ spc() ++ str"{"
+ ++ keyword "struct" ++ spc ()
+ ++ pr_id idarg ++ str"}"
+ in
+ hov 1 (str"(" ++ pr_id id ++
+ prlist pr_binder_fix bll ++ annot ++ str" :" ++
+ pr_lconstrarg ty ++ str")") in
+ (* spc() ++
+ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+ c)
+ *)
+ let pr_cofix_tac (id,c) =
+ hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
+
+ (* Printing tactics as arguments *)
+ let rec pr_atom0 a = tag_atom a (match a with
+ | TacIntroPattern [] -> primitive "intros"
+ | t -> str "(" ++ pr_atom1 t ++ str ")"
+ )
+
+ (* Main tactic printer *)
+ and pr_atom1 a = tag_atom a (match a with
+ (* Basic tactics *)
+ | TacIntroPattern [] as t ->
+ pr_atom0 t
+ | TacIntroPattern (_::_ as p) ->
+ hov 1 (primitive "intros" ++ spc () ++
+ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
+ | TacApply (a,ev,cb,inhyp) ->
+ hov 1 (
+ (if a then mt() else primitive "simple ") ++
+ primitive (with_evars ev "apply") ++ spc () ++
+ prlist_with_sep pr_comma pr_with_bindings_arg cb ++
+ pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp
+ )
+ | TacElim (ev,cb,cbo) ->
+ hov 1 (
+ primitive (with_evars ev "elim")
+ ++ pr_arg pr_with_bindings_arg cb
+ ++ pr_opt pr_eliminator cbo)
+ | TacCase (ev,cb) ->
+ hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
+ | TacMutualFix (id,n,l) ->
+ hov 1 (
+ primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
+ ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
+ | TacMutualCofix (id,l) ->
+ hov 1 (
+ primitive "cofix" ++ spc () ++ pr_id id ++ spc()
+ ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
+ )
+ | TacAssert (b,Some tac,ipat,c) ->
+ hov 1 (
+ primitive (if b then "assert" else "enough") ++
+ pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
+ pr_by_tactic (pr.pr_tactic ltop) tac
+ )
+ | TacAssert (_,None,ipat,c) ->
+ hov 1 (
+ primitive "pose proof"
+ ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
+ )
+ | TacGeneralize l ->
+ hov 1 (
+ primitive "generalize" ++ spc ()
+ ++ prlist_with_sep pr_comma (fun (cl,na) ->
+ pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
+ l
+ )
+ | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
+ hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+ | TacLetTac (na,c,cl,b,e) ->
+ hov 1 (
+ (if b then primitive "set" else primitive "remember") ++
+ (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
+ else pr_pose_as_style pr.pr_constr na c) ++
+ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
+ pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl)
+ (* | TacInstantiate (n,c,ConclLocation ()) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg c ++ str ")" ))
+ | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg c ++ str ")" )
+ ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
*)
- let pr_cofix_tac (id,c) =
- hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
-
- (* Printing tactics as arguments *)
- let rec pr_atom0 a = tag_atom a (match a with
- | TacIntroPattern [] -> primitive "intros"
- | TacIntroMove (None,MoveLast) -> primitive "intro"
- | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial"
- | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto"
- | TacClear (true,[]) -> primitive "clear"
- | t -> str "(" ++ pr_atom1 t ++ str ")"
- )
-
- (* Main tactic printer *)
- and pr_atom1 a = tag_atom a (match a with
- (* Basic tactics *)
- | TacIntroPattern [] as t ->
- pr_atom0 t
- | TacIntroPattern (_::_ as p) ->
- hov 1 (primitive "intros" ++ spc () ++
- prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
- | TacIntroMove (None,MoveLast) as t ->
- pr_atom0 t
- | TacIntroMove (Some id,MoveLast) ->
- primitive "intro" ++ spc () ++ pr_id id
- | TacIntroMove (ido,hto) ->
- hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
- Miscprint.pr_move_location pr.pr_name hto)
- | TacExact c ->
- hov 1 (primitive "exact" ++ pr_constrarg c)
- | TacApply (a,ev,cb,inhyp) ->
- hov 1 (
- (if a then mt() else primitive "simple ") ++
- primitive (with_evars ev "apply") ++ spc () ++
- prlist_with_sep pr_comma pr_with_bindings_arg cb ++
- pr_in_hyp_as pr.pr_dconstr pr.pr_name inhyp
- )
- | TacElim (ev,cb,cbo) ->
- hov 1 (
- primitive (with_evars ev "elim")
- ++ pr_arg pr_with_bindings_arg cb
- ++ pr_opt pr_eliminator cbo)
- | TacCase (ev,cb) ->
- hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
- | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
- | TacMutualFix (id,n,l) ->
- hov 1 (
- primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
- ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
- | TacCofix ido ->
- hov 1 (primitive "cofix" ++ pr_opt pr_id ido)
- | TacMutualCofix (id,l) ->
- hov 1 (
- primitive "cofix" ++ spc () ++ pr_id id ++ spc()
- ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
- )
- | TacAssert (b,Some tac,ipat,c) ->
- hov 1 (
- primitive (if b then "assert" else "enough") ++
- pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
- pr_by_tactic (pr.pr_tactic ltop) tac
- )
- | TacAssert (_,None,ipat,c) ->
- hov 1 (
- primitive "pose proof"
- ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
- )
- | TacGeneralize l ->
- hov 1 (
- primitive "generalize" ++ spc ()
- ++ prlist_with_sep pr_comma (fun (cl,na) ->
- pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
- l
- )
- | TacGeneralizeDep c ->
- hov 1 (
- primitive "generalize" ++ spc () ++ str "dependent"
- ++ pr_constrarg c
- )
- | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
- hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
- | TacLetTac (na,c,cl,b,e) ->
- hov 1 (
- (if b then primitive "set" else primitive "remember") ++
- (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
- else pr_pose_as_style pr.pr_constr na c) ++
- pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
- pr_clauses (Some b) pr.pr_name cl)
- (* | TacInstantiate (n,c,ConclLocation ()) ->
- hov 1 (str "instantiate" ++ spc() ++
- hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
- pr_lconstrarg c ++ str ")" ))
- | TacInstantiate (n,c,HypLocation (id,hloc)) ->
- hov 1 (str "instantiate" ++ spc() ++
- hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
- pr_lconstrarg c ++ str ")" )
- ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
- *)
-
- (* Derived basic tactics *)
- | TacInductionDestruct (isrec,ev,(l,el)) ->
- hov 1 (
- primitive (with_evars ev (if isrec then "induction" else "destruct"))
- ++ spc ()
- ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
- pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
- pr_with_induction_names pr.pr_dconstr ids ++
- pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++
- pr_opt pr_eliminator el
- )
- | TacDoubleInduction (h1,h2) ->
- hov 1 (
- primitive "double induction"
- ++ pr_arg pr_quantified_hypothesis h1
- ++ pr_arg pr_quantified_hypothesis h2
- )
-
- (* Automation tactics *)
- | TacTrivial (_,[],Some []) as x ->
- pr_atom0 x
- | TacTrivial (d,lems,db) ->
- hov 0 (
- str (string_of_debug d) ++ primitive "trivial"
- ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
- )
- | TacAuto (_,None,[],Some []) as x ->
- pr_atom0 x
- | TacAuto (d,n,lems,db) ->
- hov 0 (
- str (string_of_debug d) ++ primitive "auto"
- ++ pr_opt (pr_or_var int) n
- ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
- )
- (* Context management *)
- | TacClear (true,[]) as t ->
- pr_atom0 t
- | TacClear (keep,l) ->
- hov 1 (
- primitive "clear" ++ spc ()
- ++ (if keep then str "- " else mt ())
- ++ prlist_with_sep spc pr.pr_name l
- )
- | TacClearBody l ->
- hov 1 (
- primitive "clearbody" ++ spc ()
- ++ prlist_with_sep spc pr.pr_name l
- )
- | TacMove (id1,id2) ->
- hov 1 (
- primitive "move"
- ++ brk (1,1) ++ pr.pr_name id1
- ++ Miscprint.pr_move_location pr.pr_name id2
- )
- | TacRename l ->
- hov 1 (
- primitive "rename" ++ brk (1,1)
- ++ prlist_with_sep
- (fun () -> str "," ++ brk (1,1))
- (fun (i1,i2) ->
- pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
- l
- )
+ (* Derived basic tactics *)
+ | TacInductionDestruct (isrec,ev,(l,el)) ->
+ hov 1 (
+ primitive (with_evars ev (if isrec then "induction" else "destruct"))
+ ++ spc ()
+ ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
+ pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
+ pr_with_induction_names pr.pr_dconstr ids ++
+ pr_opt (pr_clauses None pr.pr_name) cl) l ++
+ pr_opt pr_eliminator el
+ )
- (* Constructors *)
- | TacSplit (ev,l) ->
- hov 1 (
- primitive (with_evars ev "exists")
- ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l
- )
+ (* Conversion *)
+ | TacReduce (r,h) ->
+ hov 1 (
+ pr_red_expr r
+ ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+ )
+ | TacChange (op,c,h) ->
+ hov 1 (
+ primitive "change" ++ brk (1,1)
+ ++ (
+ match op with
+ None ->
+ mt ()
+ | Some p ->
+ pr.pr_pattern p ++ spc ()
+ ++ keyword "with" ++ spc ()
+ ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+ )
- (* Conversion *)
- | TacReduce (r,h) ->
- hov 1 (
- pr_red_expr r
- ++ pr_clauses (Some true) pr.pr_name h
- )
- | TacChange (op,c,h) ->
- hov 1 (
- primitive "change" ++ brk (1,1)
- ++ (
- match op with
- None ->
- mt ()
- | Some p ->
- pr.pr_pattern p ++ spc ()
- ++ keyword "with" ++ spc ()
- ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h
+ (* Equality and inversion *)
+ | TacRewrite (ev,l,cl,by) ->
+ hov 1 (
+ primitive (with_evars ev "rewrite") ++ spc ()
+ ++ prlist_with_sep
+ (fun () -> str ","++spc())
+ (fun (b,m,c) ->
+ pr_orient b ++ pr_multi m ++
+ pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
+ l
+ ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
+ ++ (
+ match by with
+ | Some by -> pr_by_tactic (pr.pr_tactic ltop) by
+ | None -> mt()
)
+ )
+ | TacInversion (DepInversion (k,c,ids),hyp) ->
+ hov 1 (
+ primitive "dependent " ++ pr_induction_kind k ++ spc ()
+ ++ pr_quantified_hypothesis hyp
+ ++ pr_with_inversion_names pr.pr_dconstr ids
+ ++ pr_with_constr pr.pr_constr c
+ )
+ | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+ hov 1 (
+ pr_induction_kind k ++ spc ()
+ ++ pr_quantified_hypothesis hyp
+ ++ pr_with_inversion_names pr.pr_dconstr ids
+ ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+ )
+ | TacInversion (InversionUsing (c,cl),hyp) ->
+ hov 1 (
+ primitive "inversion" ++ spc()
+ ++ pr_quantified_hypothesis hyp ++ spc ()
+ ++ keyword "using" ++ spc () ++ pr.pr_constr c
+ ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+ )
+ )
+ in
+ pr_atom1
- (* Equivalence relations *)
- | TacSymmetry cls ->
- primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls
-
- (* Equality and inversion *)
- | TacRewrite (ev,l,cl,by) ->
- hov 1 (
- primitive (with_evars ev "rewrite") ++ spc ()
- ++ prlist_with_sep
- (fun () -> str ","++spc())
- (fun (b,m,c) ->
- pr_orient b ++ pr_multi m ++
- pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
- l
- ++ pr_clauses (Some true) pr.pr_name cl
- ++ (
- match by with
- | Some by -> pr_by_tactic (pr.pr_tactic ltop) by
- | None -> mt()
- )
- )
- | TacInversion (DepInversion (k,c,ids),hyp) ->
- hov 1 (
- primitive "dependent " ++ pr_induction_kind k ++ spc ()
- ++ pr_quantified_hypothesis hyp
- ++ pr_with_inversion_names pr.pr_dconstr ids
- ++ pr_with_constr pr.pr_constr c
- )
- | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
- hov 1 (
- pr_induction_kind k ++ spc ()
- ++ pr_quantified_hypothesis hyp
- ++ pr_with_inversion_names pr.pr_dconstr ids
- ++ pr_simple_hyp_clause pr.pr_name cl
- )
- | TacInversion (InversionUsing (c,cl),hyp) ->
- hov 1 (
- primitive "inversion" ++ spc()
- ++ pr_quantified_hypothesis hyp ++ spc ()
- ++ keyword "using" ++ spc () ++ pr.pr_constr c
- ++ pr_simple_hyp_clause pr.pr_name cl
- )
- )
- in
+ let make_pr_tac pr strip_prod_binders tag_atom tag =
+ let extract_binders = function
+ | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+ | body -> ([],body) in
let rec pr_tac inherited tac =
let return (doc, l) = (tag tac doc, l) in
let (strm, prec) = return (match tac with
@@ -1234,7 +1140,7 @@ module Make
| TacId l ->
keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
| TacAtom (loc,t) ->
- pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
+ pr_with_comments loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
| TacArg(_,Tacexp e) ->
pr.pr_tactic (latom,E) e, latom
| TacArg(_,ConstrMayEval (ConstrTerm c)) ->
@@ -1257,26 +1163,17 @@ module Make
| TacML (loc,s,l) ->
pr_with_comments loc (pr.pr_extend 1 s l), lcall
| TacAlias (loc,kn,l) ->
- pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
+ pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom
)
in
if prec_less prec inherited then strm
else str"(" ++ strm ++ str")"
and pr_tacarg = function
- | TacDynamic (loc,t) ->
- pr_with_comments loc
- (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
- | MetaIdArg (loc,true,s) ->
- pr_with_comments loc (str "$" ++ str s)
- | MetaIdArg (loc,false,s) ->
- pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
| Reference r ->
pr.pr_reference r
| ConstrMayEval c ->
pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
- | UConstr c ->
- keyword "uconstr:" ++ pr.pr_uconstr c
| TacFreshId l ->
keyword "fresh" ++ pr_fresh_ids l
| TacPretype c ->
@@ -1304,7 +1201,6 @@ module Make
let pr = {
pr_tactic = pr_raw_tactic_level;
pr_constr = pr_constr_expr;
- pr_uconstr = pr_constr_expr;
pr_dconstr = pr_constr_expr;
pr_lconstr = pr_lconstr_expr;
pr_pattern = pr_constr_pattern_expr;
@@ -1312,8 +1208,8 @@ module Make
pr_constant = pr_or_by_notation pr_reference;
pr_reference = pr_reference;
pr_name = pr_lident;
- pr_generic = Genprint.generic_raw_print;
- pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+ pr_generic = pr_raw_generic_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference;
+ pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
} in
make_pr_tac
@@ -1325,9 +1221,9 @@ module Make
let pr_and_constr_expr pr (c,_) = pr c
- let pr_pat_and_constr_expr pr ((c,_),_) = pr c
+ let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c
- let rec pr_glob_tactic_level env n t =
+ let pr_glob_tactic_level env n t =
let glob_printers =
(strip_prod_binders_glob_constr)
in
@@ -1335,7 +1231,6 @@ module Make
let pr = {
pr_tactic = prtac;
pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
- pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env);
pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
@@ -1343,8 +1238,10 @@ module Make
pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
pr_name = pr_lident;
- pr_generic = Genprint.generic_glb_print;
- pr_extend = pr_glob_extend
+ pr_generic = pr_glb_generic_rec
+ (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+ prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+ pr_extend = pr_glob_extend_rec
(pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
pr_alias = pr_glob_alias
@@ -1369,39 +1266,49 @@ module Make
| _ -> error "Cannot translate fix tactic: not enough products" in
strip_ty [] n ty
- let pr_tactic_level env n t =
- let typed_printers =
- (strip_prod_binders_constr)
- in
- let prtac n (t:tactic_expr) =
+ let pr_atomic_tactic_level env n t =
+ let prtac n (t:atomic_tactic_expr) =
let pr = {
- pr_tactic = pr_glob_tactic_level env;
+ pr_tactic = (fun _ _ -> str "<tactic>");
pr_constr = pr_constr_env env Evd.empty;
- pr_uconstr = pr_closed_glob_env env Evd.empty;
pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
pr_lconstr = pr_lconstr_env env Evd.empty;
- pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
- pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
- pr_constant = pr_and_short_name (pr_evaluable_reference_env env);
+ pr_pattern = pr_constr_pattern_env env Evd.empty;
+ pr_lpattern = pr_lconstr_pattern_env env Evd.empty;
+ pr_constant = pr_evaluable_reference_env env;
pr_reference = pr_located pr_ltac_constant;
pr_name = pr_id;
- pr_generic = Genprint.generic_top_print;
- pr_extend = pr_extend
- (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern;
- pr_alias = pr_alias
- (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern;
+ (** Those are not used by the atomic printer *)
+ pr_generic = (fun _ -> assert false);
+ pr_extend = (fun _ _ _ -> assert false);
+ pr_alias = (fun _ _ _ -> assert false);
}
in
- make_pr_tac
- pr typed_printers
- tag_atomic_tactic_expr tag_tactic_expr
- n t
+ pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
in
prtac n t
- let pr_tactic env = pr_tactic_level env ltop
+ let pr_raw_generic env = pr_raw_generic_rec
+ pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference
+
+ let pr_glb_generic env = pr_glb_generic_rec
+ (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+ (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+
+ let pr_raw_extend env = pr_raw_extend_rec
+ pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
+
+ let pr_glob_extend env = pr_glob_extend_rec
+ (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+ (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+
+ let pr_alias pr lev key args =
+ pr_alias_gen (fun _ arg -> pr arg) lev key args
+
+ let pr_extend pr lev ml args =
+ pr_extend_gen pr lev ml args
+
+ let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
end
@@ -1431,37 +1338,68 @@ include Make (Ppconstr) (struct
let tag_glob_atomic_tactic_expr = do_not_tag
let tag_raw_tactic_expr = do_not_tag
let tag_raw_atomic_tactic_expr = do_not_tag
- let tag_tactic_expr = do_not_tag
let tag_atomic_tactic_expr = do_not_tag
end)
(** Registering *)
+let run_delayed c =
+ Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma }
+
let () =
let pr_bool b = if b then str "true" else str "false" in
let pr_unit _ = str "()" in
let pr_string s = str "\"" ++ str s ++ str "\"" in
+ Genprint.register_print0 Constrarg.wit_int_or_var
+ (pr_or_var int) (pr_or_var int) int;
Genprint.register_print0 Constrarg.wit_ref
pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+ Genprint.register_print0 Constrarg.wit_ident
+ pr_id pr_id pr_id;
+ Genprint.register_print0 Constrarg.wit_var
+ (pr_located pr_id) (pr_located pr_id) pr_id;
Genprint.register_print0
Constrarg.wit_intro_pattern
(Miscprint.pr_intro_pattern pr_constr_expr)
(Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
- (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty))));
+ (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c))));
Genprint.register_print0
Constrarg.wit_clause_dft_concl
(pr_clauses (Some true) pr_lident)
(pr_clauses (Some true) pr_lident)
(pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
;
- Genprint.register_print0 Constrarg.wit_sort
- pr_glob_sort pr_glob_sort (pr_sort Evd.empty);
+ Genprint.register_print0
+ Constrarg.wit_constr
+ Ppconstr.pr_constr_expr
+ (fun (c, _) -> Printer.pr_glob_constr c)
+ Printer.pr_constr
+ ;
Genprint.register_print0
Constrarg.wit_uconstr
Ppconstr.pr_constr_expr
(fun (c,_) -> Printer.pr_glob_constr c)
Printer.pr_closed_glob
;
+ Genprint.register_print0
+ Constrarg.wit_open_constr
+ Ppconstr.pr_constr_expr
+ (fun (c, _) -> Printer.pr_glob_constr c)
+ Printer.pr_constr
+ ;
+ Genprint.register_print0 Constrarg.wit_red_expr
+ (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
+ (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
+ (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern));
+ Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+ Genprint.register_print0 Constrarg.wit_bindings
+ (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
+ (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
+ Genprint.register_print0 Constrarg.wit_constr_with_bindings
+ (pr_with_bindings pr_constr_expr pr_lconstr_expr)
+ (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
Genprint.register_print0 Stdarg.wit_int int int int;
Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
@@ -1472,16 +1410,10 @@ let () =
let printer _ _ prtac = prtac (0, E) in
declare_extra_genarg_pprule wit_tactic printer printer printer
-let _ = Hook.set Tactic_debug.tactic_printer
- (fun x -> pr_glob_tactic (Global.env()) x)
-
-let _ = Hook.set Tactic_debug.match_pattern_printer
- (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp)
-
-let _ = Hook.set Tactic_debug.match_rule_printer
- (fun rl ->
- pr_match_rule false (pr_glob_tactic (Global.env()))
- (fun (_,p) -> pr_constr_pattern p) rl)
+let () =
+ let pr_unit _ _ _ () = str "()" in
+ let printer _ _ prtac = prtac (0, E) in
+ declare_extra_genarg_pprule wit_ltac printer printer pr_unit
module Richpp = struct
@@ -1496,7 +1428,6 @@ module Richpp = struct
let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a)
let tag_raw_tactic_expr e = tag (ARawTacticExpr e)
let tag_raw_atomic_tactic_expr a = tag (ARawAtomicTacticExpr a)
- let tag_tactic_expr e = tag (ATacticExpr e)
let tag_atomic_tactic_expr a = tag (AAtomicTacticExpr a)
end)
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 30b9483db7..86e3ea5484 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -11,11 +11,15 @@
open Pp
open Genarg
+open Geninterp
open Names
open Constrexpr
open Tacexpr
open Ppextend
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) ->
@@ -32,7 +36,7 @@ type 'a glob_extra_genarg_printer =
type 'a extra_genarg_printer =
(Term.constr -> std_ppcmds) ->
(Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ (tolerability -> Val.t -> std_ppcmds) ->
'a -> std_ppcmds
val declare_extra_genarg_pprule :
@@ -41,14 +45,13 @@ val declare_extra_genarg_pprule :
'b glob_extra_genarg_printer ->
'c extra_genarg_printer -> unit
-type grammar_terminals = string option list
+type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
type pp_tactic = {
- pptac_args : argument_type list;
- pptac_prods : int * grammar_terminals;
+ pptac_level : int;
+ pptac_prods : grammar_terminals;
}
-val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
(** The default pretty-printers produce {!Pp.std_ppcmds} that are
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 1631bda377..c08d6044db 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,11 +8,10 @@
open Pp
open Genarg
-open Constrexpr
+open Geninterp
open Tacexpr
open Ppextend
open Environ
-open Pattern
open Misctypes
module type Pp = sig
@@ -32,46 +31,26 @@ module type Pp = sig
val pr_clauses : bool option ->
('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
- val pr_raw_generic :
- (constr_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- (Libnames.reference -> std_ppcmds) -> rlevel generic_argument ->
- std_ppcmds
-
- val pr_glb_generic :
- (glob_constr_and_expr -> Pp.std_ppcmds) ->
- (glob_constr_and_expr -> Pp.std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (glob_constr_pattern_and_expr -> std_ppcmds) ->
- glevel generic_argument -> std_ppcmds
-
- val pr_top_generic :
- (Term.constr -> std_ppcmds) ->
- (Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (Pattern.constr_pattern -> std_ppcmds) ->
- tlevel generic_argument ->
- std_ppcmds
-
- val pr_raw_extend:
- (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) -> int ->
- ml_tactic_entry -> raw_generic_argument list -> std_ppcmds
-
- val pr_glob_extend:
- (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (glob_constr_pattern_and_expr -> std_ppcmds) -> int ->
- ml_tactic_entry -> glob_generic_argument list -> std_ppcmds
+
+ val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+
+ val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+
+ val pr_raw_extend: env -> int ->
+ ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+
+ val pr_glob_extend: env -> int ->
+ ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
val pr_extend :
- (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (constr_pattern -> std_ppcmds) -> int ->
- ml_tactic_entry -> typed_generic_argument list -> std_ppcmds
+ (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+
+ val pr_alias_key : Names.KerName.t -> std_ppcmds
+
+ val pr_alias : (Val.t -> std_ppcmds) ->
+ int -> Names.KerName.t -> Val.t list -> std_ppcmds
+
+ val pr_alias_key : Names.KerName.t -> std_ppcmds
val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
@@ -81,7 +60,7 @@ module type Pp = sig
val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
- val pr_tactic : env -> tactic_expr -> std_ppcmds
+ val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
val pr_hintbases : string list option -> std_ppcmds
@@ -91,4 +70,11 @@ module type Pp = sig
('constr -> std_ppcmds) ->
('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
+ val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+ val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+ ('b, 'a) match_rule -> std_ppcmds
+
+ val pr_value : tolerability -> Val.t -> std_ppcmds
+
end
diff --git a/printing/pputils.ml b/printing/pputils.ml
index ee1a39efd3..906b463a85 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 7287748327..a0f2c77283 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 832c08fe0e..cd7434843f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -43,6 +43,12 @@ module Make
else
pr_id id
+ let pr_plident (lid, l) =
+ pr_lident lid ++
+ (match l with
+ | Some l -> prlist_with_sep spc pr_lident l
+ | None -> mt())
+
let string_of_fqid fqid =
String.concat "." (List.map Id.to_string fqid)
@@ -73,13 +79,7 @@ module Make
| VernacEndSubproof -> str""
| _ -> str"."
- let pr_gen t =
- pr_raw_generic
- pr_constr_expr
- pr_lconstr_expr
- pr_raw_tactic_level
- pr_constr_expr
- pr_reference t
+ let pr_gen t = pr_raw_generic (Global.env ()) t
let sep = fun _ -> spc()
let sep_v2 = fun _ -> str"," ++ spc()
@@ -99,18 +99,6 @@ module Make
| ETBinder false -> str "closed binder"
| ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
- let strip_meta id =
- let s = Id.to_string id in
- if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1))
- else id
-
- let pr_production_item = function
- | TacNonTerm (loc,nt,Some (p,sep)) ->
- let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in
- str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
- | TacNonTerm (loc,nt,None) -> str nt
- | TacTerm s -> qs s
-
let pr_comment pr_c = function
| CommentConstr c -> pr_c c
| CommentString s -> qs s
@@ -160,6 +148,8 @@ module Make
(* This should not happen because of the grammar *)
| IntValue (Some n) -> spc() ++ int n
| StringValue s -> spc() ++ str s
+ | StringOptValue None -> mt()
+ | StringOptValue (Some s) -> spc() ++ str s
| BoolValue b -> mt()
in pr_printoption a None ++ pr_opt_value b
@@ -348,6 +338,7 @@ module Make
| l ->
prlist_with_sep spc
(fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
+
(*
prlist_with_sep pr_semicolon (pr_params pr_c)
*)
@@ -366,6 +357,7 @@ module Make
| SetAssoc RightA -> keyword "right associativity"
| SetAssoc NonA -> keyword "no associativity"
| SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
+ | SetOnlyPrinting -> keyword "only printing"
| SetOnlyParsing Flags.Current -> keyword "only parsing"
| SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
| SetFormat("text",s) -> keyword "format " ++ pr_located qs s
@@ -376,21 +368,16 @@ module Make
| l -> spc() ++
hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
- let print_level n =
- if not (Int.equal n 0) then
- spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")")
- else
- mt ()
-
- let pr_grammar_tactic_rule n (_,pil,t) =
- hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++
- hov 0 (prlist_with_sep sep pr_production_item pil ++
- spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
+ let pr_univs pl =
+ match pl with
+ | None -> mt ()
+ | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
- let pr_statement head (id,(bl,c,guard)) =
- assert (not (Option.is_empty id));
+ let pr_statement head (idpl,(bl,c,guard)) =
+ assert (not (Option.is_empty idpl));
+ let id, pl = Option.get idpl in
hov 2
- (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
+ (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
(match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
str":" ++ pr_spc_lconstr c)
@@ -458,8 +445,6 @@ module Make
keyword "Print TypeClasses"
| PrintInstances qid ->
keyword "Print Instances" ++ spc () ++ pr_smart_global qid
- | PrintLtac qid ->
- keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid
| PrintCoercions ->
keyword "Print Coercions"
| PrintCoercionPaths (s,t) ->
@@ -478,8 +463,6 @@ module Make
keyword "Print Hint *"
| PrintHintDbName s ->
keyword "Print HintDb" ++ spc () ++ str s
- | PrintRewriteHintDbName s ->
- keyword "Print Rewrite HintDb" ++ spc() ++ str s
| PrintUniverses (b, fopt) ->
let cmd =
if b then "Print Sorted Universes"
@@ -579,7 +562,8 @@ module Make
let pr_goal_reference = function
| OpenSubgoals -> mt ()
| NthGoal n -> spc () ++ int n
- | GoalId n -> spc () ++ str n in
+ | GoalId id -> spc () ++ pr_id id
+ | 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
@@ -625,10 +609,10 @@ module Make
else
spc() ++ qs s
)
- | VernacTime v ->
- return (keyword "Time" ++ spc() ++ pr_vernac_list v)
- | VernacRedirect (s, v) ->
- return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v)
+ | VernacTime (_,v) ->
+ return (keyword "Time" ++ spc() ++ pr_vernac v)
+ | VernacRedirect (s, (_,v)) ->
+ return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac v)
| VernacTimeout(n,v) ->
return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
| VernacFail v ->
@@ -637,22 +621,24 @@ module Make
return (keyword "No-parsing-rule for VernacError")
(* Syntax *)
- | VernacTacticNotation (n,r,e) ->
- return (pr_grammar_tactic_rule n ("",r,e))
| VernacOpenCloseScope (_,(opening,sc)) ->
return (
keyword (if opening then "Open " else "Close ") ++
keyword "Scope" ++ spc() ++ str sc
)
- | VernacDelimiters (sc,key) ->
+ | VernacDelimiters (sc,Some key) ->
return (
keyword "Delimit Scope" ++ spc () ++ str sc ++
spc() ++ keyword "with" ++ spc () ++ str key
)
+ | VernacDelimiters (sc, None) ->
+ return (
+ keyword "Undelimit Scope" ++ spc () ++ str sc
+ )
| VernacBindScope (sc,cll) ->
return (
keyword "Bind Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_smart_global cll
+ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
)
| VernacArgumentsScope (q,scl) ->
let pr_opt_scope = function
@@ -725,7 +711,7 @@ module Make
return (
hov 2 (
pr_def_token d ++ spc()
- ++ pr_lident id ++ binds ++ typ
+ ++ pr_plident id ++ binds ++ typ
++ (match c with
| None -> mt()
| Some cc -> str" :=" ++ spc() ++ cc))
@@ -756,11 +742,12 @@ module Make
return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
| VernacAssumption (stre,_,l) ->
let n = List.length (List.flatten (List.map fst (List.map snd l))) in
- return (
- hov 2
- (pr_assumption_token (n > 1) stre ++ spc() ++
- pr_ne_params_list pr_lconstr_expr l)
- )
+ let pr_params (c, (xl, t)) =
+ hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++
+ (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t))
+ in
+ let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
+ return (hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ assumptions))
| VernacInductive (p,f,l) ->
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
@@ -777,12 +764,12 @@ module Make
| RecordDecl (c,fs) ->
pr_record_decl b c fs
in
- let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+ let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) =
hov 0 (
str key ++ spc() ++
- (if coe then str"> " else str"") ++ pr_lident id ++
- pr_and_type_binders_arg indpar ++ spc() ++
- Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
+ (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++
+ pr_and_type_binders_arg indpar ++
+ pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
str" :=") ++ pr_constructor_list k lc ++
prlist (pr_decl_notation pr_constr) ntn
in
@@ -804,9 +791,9 @@ module Make
| None | Some Global -> ""
in
let pr_onerec = function
- | ((loc,id),ro,bl,type_,def),ntn ->
+ | (((loc,id),pl),ro,bl,type_,def),ntn ->
let annot = pr_guard_annot pr_lconstr_expr bl ro in
- pr_id id ++ pr_binders_arg bl ++ annot
+ pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
prlist (pr_decl_notation pr_constr) ntn
@@ -822,8 +809,8 @@ module Make
| Some Local -> keyword "Local" ++ spc ()
| None | Some Global -> str ""
in
- let pr_onecorec (((loc,id),bl,c,def),ntn) =
- pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+ let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) =
+ pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
spc() ++ pr_lconstr_expr c ++
pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
prlist (pr_decl_notation pr_constr) ntn
@@ -904,8 +891,9 @@ module Make
hov 1 (
(if abst then keyword "Declare" ++ spc () else mt ()) ++
keyword "Instance" ++
- (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
- Anonymous -> mt ()) ++
+ (match instid with
+ | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc ()
+ | (_, Anonymous), _ -> mt ()) ++
pr_and_type_binders_arg sup ++
str":" ++ spc () ++
pr_constr cl ++ pr_priority pri ++
@@ -966,24 +954,6 @@ module Make
prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
)
(* Solving *)
- | VernacSolve (i,info,tac,deftac) ->
- let pr_goal_selector = function
- | SelectNth i -> int i ++ str":"
- | SelectId id -> pr_id id ++ str":"
- | SelectAll -> str"all" ++ str":"
- | SelectAllParallel -> str"par"
- in
- let pr_info =
- match info with
- | None -> mt ()
- | Some i -> str"Info"++spc()++int i++spc()
- in
- return (
- (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++
- pr_info ++
- pr_raw_tactic tac
- ++ (if deftac then str ".." else mt ())
- )
| VernacSolveExistential (i,c) ->
return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
@@ -1015,24 +985,6 @@ module Make
return (keyword "Cd" ++ pr_opt qs s)
(* Commands *)
- | VernacDeclareTacticDefinition (rc,l) ->
- let pr_tac_body (id, redef, body) =
- let idl, body =
- match body with
- | Tacexpr.TacFun (idl,b) -> idl,b
- | _ -> [], body in
- pr_ltac_ref id ++
- prlist (function None -> str " _"
- | Some id -> spc () ++ pr_id id) idl
- ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
- pr_raw_tactic body
- in
- return (
- hov 1
- (keyword "Ltac" ++ spc () ++
- prlist_with_sep (fun () ->
- fnl() ++ keyword "with" ++ spc ()) pr_tac_body l)
- )
| VernacCreateHintDb (dbname,b) ->
return (
hov 1 (keyword "Create HintDb" ++ spc () ++
@@ -1209,8 +1161,6 @@ module Make
(keyword "Comments" ++ spc()
++ prlist_with_sep sep (pr_comment pr_constr) l)
)
- | VernacNop ->
- mt()
(* Toplevel control *)
| VernacToplevelControl exn ->
@@ -1247,33 +1197,21 @@ module Make
| VernacEndSubproof ->
return (str "}")
- and pr_vernac_list l =
- hov 2 (str"[" ++ spc() ++
- prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l
- ++ spc() ++ str"]")
-
and pr_extend s cl =
let pr_arg a =
try pr_gen a
with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
try
let rl = Egramml.get_extend_vernac_rule s in
- let start,rl,cl =
- match rl with
- | Egramml.GramTerminal s :: rl -> str s, rl, cl
- | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl
- | [] -> anomaly (Pp.str "Empty entry") in
- let (pp,_) =
- List.fold_left
- (fun (strm,args) pi ->
- let pp,args = match pi with
- | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args)
- | Egramml.GramTerminal s -> (str s, args) in
- (strm ++ spc() ++ pp), args)
- (start,cl) rl in
- hov 1 pp
+ let rec aux rl cl =
+ match rl, cl with
+ | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
+ | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
+ | [], [] -> []
+ | _ -> assert false in
+ hov 1 (pr_sequence (fun x -> x) (aux rl cl))
with Not_found ->
- hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+ hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
in pr_vernac
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index f38848cdcf..d3d4a5ceb7 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli
index cfcd49744e..5d1c89332c 100644
--- a/printing/ppvernacsig.mli
+++ b/printing/ppvernacsig.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e50435cda2..9745a79250 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -35,7 +35,7 @@ type object_pr = {
print_syntactic_def : kernel_name -> std_ppcmds;
print_module : bool -> Names.module_path -> std_ppcmds;
print_modtype : module_path -> std_ppcmds;
- print_named_decl : Id.t * constr option * types -> std_ppcmds;
+ 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;
@@ -73,8 +73,15 @@ let print_ref reduce ref =
in it_mkProd_or_LetIn ccl ctx
else typ in
let univs = Global.universes_of_global ref in
- hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++
- Printer.pr_universe_ctx univs)
+ let env = Global.env () in
+ let bl = Universes.universe_binders_of_global ref in
+ let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
+ let inst =
+ 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 ++
+ Printer.pr_universe_ctx sigma univs)
(********************************)
(** Printing implicit arguments *)
@@ -125,7 +132,8 @@ 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 nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) 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
List.exists is_status_implicit lastimpl
@@ -161,8 +169,10 @@ type opacity =
| FullyOpaque
| TransparentMaybeOpacified of Conv_oracle.level
-let opacity env = function
- | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) ->
+let opacity env =
+ let open Context.Named.Declaration in
+ function
+ | VarRef v when is_local_def (Environ.lookup_named v env) ->
Some(TransparentMaybeOpacified
(Conv_oracle.get_strategy (Environ.oracle env) (VarKey v)))
| ConstRef cst ->
@@ -205,16 +215,20 @@ let print_polymorphism ref =
else "not universe polymorphic") ]
else []
-let print_primitive_record mipv = function
+let print_primitive_record recflag mipv = function
| Some (Some (_, ps,_)) ->
- [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."]
+ let eta = match recflag with
+ | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
+ | Decl_kinds.BiFinite -> str " and has eta conversion"
+ in
+ [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
| _ -> []
let print_primitive ref =
match ref with
| IndRef ind ->
let mib,_ = Global.lookup_inductive ind in
- print_primitive_record mib.mind_packets mib.mind_record
+ print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record
| _ -> []
let print_name_infos ref =
@@ -429,11 +443,13 @@ let print_named_def name body typ =
let print_named_assum name typ =
str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
-let gallina_print_named_decl (id,c,typ) =
- let s = Id.to_string id in
- match c with
- | Some body -> print_named_def s body typ
- | None -> print_named_assum s typ
+let gallina_print_named_decl =
+ let open Context.Named.Declaration in
+ function
+ | LocalAssum (id, typ) ->
+ print_named_assum (Id.to_string id) typ
+ | LocalDef (id, body, typ) ->
+ print_named_def (Id.to_string id) body typ
let assumptions_for_print lna =
List.fold_right (fun na env -> add_name na env) lna empty_names_context
@@ -447,7 +463,7 @@ let gallina_print_inductive sp =
let mipv = mib.mind_packets in
pr_mutual_inductive_body env sp mib ++
with_line_skip
- (print_primitive_record mipv mib.mind_record @
+ (print_primitive_record mib.mind_finite mipv mib.mind_record @
print_inductive_renames sp mipv @
print_inductive_implicit_args sp mipv @
print_inductive_argument_scopes sp mipv)
@@ -459,16 +475,21 @@ let gallina_print_section_variable id =
print_named_decl id ++
with_line_skip (print_name_infos (VarRef id))
-let print_body = function
- | Some c -> pr_lconstr c
+let print_body env evd = function
+ | Some c -> pr_lconstr_env env evd c
| None -> (str"<no body>")
-let print_typed_body (val_0,typ) =
- (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ)
+let print_typed_body env evd (val_0,typ) =
+ (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ)
let ungeneralized_type_of_constant_type t =
Typeops.type_of_constant_type (Global.env ()) t
+let print_instance sigma cb =
+ if cb.const_polymorphic then
+ pr_universe_instance sigma cb.const_universes
+ else mt()
+
let print_constant with_values sep sp =
let cb = Global.lookup_constant sp in
let val_0 = Global.body_of_constant_body cb in
@@ -477,17 +498,23 @@ let print_constant with_values sep sp =
let univs = Univ.instantiate_univ_context
(Global.universes_of_constant_body cb)
in
+ let ctx =
+ Evd.evar_universe_context_of_binders
+ (Universes.universe_binders_of_global (ConstRef sp))
+ in
+ let env = Global.env () and sigma = Evd.from_ctx ctx in
+ let pr_ltype = pr_ltype_env env sigma in
hov 0 (pr_polymorphic cb.const_polymorphic ++
match val_0 with
| None ->
str"*** [ " ++
- print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
+ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
str" ]" ++
- Printer.pr_universe_ctx univs
+ Printer.pr_universe_ctx sigma univs
| _ ->
- print_basename sp ++ str sep ++ cut () ++
- (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
- Printer.pr_universe_ctx univs)
+ print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
+ (if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++
+ Printer.pr_universe_ctx sigma univs)
let gallina_print_constant_with_infos sp =
print_constant true " = " sp ++
@@ -699,8 +726,8 @@ 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 (_,c,typ) = Global.lookup_named str in
- (print_named_decl (str,c,typ))
+ let open Context.Named.Declaration in
+ str |> Global.lookup_named |> set_id str |> print_named_decl
with Not_found ->
errorlabstrm
"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
@@ -728,8 +755,8 @@ let print_opaque_name qid =
let ty = Universes.unsafe_type_of_global gr in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
- let (_,c,ty) = lookup_named id env in
- print_named_decl (id,c,ty)
+ let open Context.Named.Declaration in
+ lookup_named id env |> set_id id |> print_named_decl
let print_about_any loc k =
match k with
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 6216d4d531..0eab155796 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -66,7 +66,7 @@ type object_pr = {
print_syntactic_def : kernel_name -> std_ppcmds;
print_module : bool -> Names.module_path -> std_ppcmds;
print_modtype : module_path -> std_ppcmds;
- print_named_decl : Id.t * constr option * types -> std_ppcmds;
+ 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;
diff --git a/printing/printer.ml b/printing/printer.ml
index 8609b19c9a..2357ca0eaa 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -28,9 +28,7 @@ let delayed_emacs_cmd s =
if !Flags.print_emacs then s () else str ""
let get_current_context () =
- try Pfedit.get_current_goal_context ()
- with e when Logic.catchable_exception e ->
- (Evd.empty, Global.env())
+ Pfedit.get_current_context ()
(**********************************************************************)
(** Terms *)
@@ -50,7 +48,7 @@ let pr_lconstr_core goal_concl_style env sigma t =
let pr_lconstr_env env = pr_lconstr_core false env
let pr_constr_env env = pr_constr_core false env
-let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env
+let _ = Hook.set Refine.pr_constr pr_constr_env
let pr_lconstr_goal_style_env env = pr_lconstr_core true env
let pr_constr_goal_style_env env = pr_constr_core true env
@@ -208,10 +206,10 @@ let safe_pr_constr t =
let (sigma, env) = get_current_context () in
safe_pr_constr_env env sigma t
-let pr_universe_ctx c =
+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 Universes.pr_with_global_universes c)) c
+ (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c
else
mt()
@@ -262,16 +260,19 @@ let pr_var_decl_skel pr_id env sigma (id,c,typ) =
let ptyp = (str" : " ++ pt) in
(pr_id id ++ hov 0 (pbody ++ ptyp))
-let pr_var_decl env sigma (id,c,typ) =
- pr_var_decl_skel pr_id env sigma (id,c,typ)
+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))
-let pr_rel_decl env sigma (na,c,typ) =
- let pbody = match c with
- | None -> mt ()
- | Some c ->
+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 pbody = match decl with
+ | LocalAssum _ -> mt ()
+ | LocalDef (_,c,_) ->
(* Force evaluation *)
let pb = pr_lconstr_env env sigma c in
let pb = if isCast c then surround pb else pb in
@@ -293,7 +294,7 @@ let pr_named_context_of env sigma =
hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
let pr_named_context env sigma ne_context =
- hv 0 (Context.fold_named_context
+ hv 0 (Context.Named.fold_outside
(fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d)
ne_context ~init:(mt ()))
@@ -306,7 +307,7 @@ let pr_rel_context_of env sigma =
(* Prints an env (variables and de Bruijn). Separator: newline *)
let pr_context_unlimited env sigma =
let sign_env =
- Context.fold_named_list_context
+ Context.NamedList.fold
(fun d pps ->
let pidt = pr_var_list_decl env sigma d in
(pps ++ fnl () ++ pidt))
@@ -333,7 +334,7 @@ let pr_context_limit n env sigma =
else
let k = lgsign-n in
let _,sign_env =
- Context.fold_named_list_context
+ Context.NamedList.fold
(fun d (i,pps) ->
if i < k then
(i+1, (pps ++str "."))
@@ -380,16 +381,12 @@ let pr_transparent_state (ids, csts) =
let default_pr_goal gs =
let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
let env = Goal.V82.env sigma g in
- let preamb,thesis,penv,pc =
- mt (), mt (),
- pr_context_of env sigma,
- pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
- in
- preamb ++
- str" " ++ hv 0 (penv ++ fnl () ++
- str (emacs_str "") ++
- str "============================" ++ fnl () ++
- thesis ++ str " " ++ pc)
+ let concl = Goal.V82.concl sigma g in
+ let goal =
+ pr_context_of env sigma ++ cut () ++
+ str "============================" ++ cut () ++
+ pr_goal_concl_style_env env sigma concl in
+ str " " ++ v 0 goal
(* display a goal tag *)
let pr_goal_tag g =
@@ -400,7 +397,7 @@ let display_name = false
(* display a goal name *)
let pr_goal_name sigma g =
- if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma))
+ if display_name then str " " ++ Pp.surround (pr_existential_key sigma g)
else mt ()
(* display the conclusion of a goal *)
@@ -420,7 +417,8 @@ let pr_evgl_sign sigma evi =
| None -> [], []
| Some f -> List.filter2 (fun b c -> not b) f (evar_context evi)
in
- let ids = List.rev_map pi1 l in
+ let open Context.Named.Declaration in
+ let ids = List.rev_map 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)")
@@ -455,14 +453,17 @@ let pr_ne_evar_set hd tl sigma l =
else
mt ()
+let pr_selected_subgoal name sigma g =
+ let pg = default_pr_goal { sigma=sigma ; it=g; } in
+ v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g
+ ++ str " is:" ++ cut () ++ pg)
+
let default_pr_subgoal n sigma =
let rec prrec p = function
| [] -> error "No such goal."
| g::rest ->
if Int.equal p 1 then
- let pg = default_pr_goal { sigma=sigma ; it=g; } in
- v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g
- ++ str " is:" ++ cut () ++ pg)
+ pr_selected_subgoal (int n) sigma g
else
prrec (p-1) rest
in
@@ -547,7 +548,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
(* Side effect! This has to be made more robust *)
let () =
match close_cmd with
- | Some cmd -> msg_info cmd
+ | Some cmd -> Feedback.msg_info cmd
| None -> ()
in
match goals with
@@ -625,19 +626,19 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
begin match bgoals,shelf,given_up with
| [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
| [] , [] , _ ->
- msg_info (str "No more subgoals, but there are some goals you gave up:");
+ Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:");
fnl ()
++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
++ fnl () ++ str "You need to go back and solve them."
| [] , _ , _ ->
- msg_info (str "All the remaining goals are on the shelf.");
+ Feedback.msg_info (str "All the remaining goals are on the shelf.");
fnl ()
++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
| _ , _, _ ->
let end_cmd =
str "This subproof is complete, but there are some unfocused goals." ++
- (match Proof_global.Bullet.suggest p
- with None -> str"" | Some s -> fnl () ++ str s) ++
+ (let s = Proof_global.Bullet.suggest p in
+ if Pp.is_empty s then s else fnl () ++ s) ++
fnl ()
in
pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
@@ -652,9 +653,17 @@ let pr_nth_open_subgoal n =
let pr_goal_by_id id =
let p = Proof_global.give_me_the_proof () in
- let g = Goal.get_by_uid id in
+ try
+ Proof.in_proof p (fun sigma ->
+ let g = Evd.evar_key id sigma in
+ pr_selected_subgoal (pr_id id) sigma g)
+ with Not_found -> error "No such goal."
+
+let pr_goal_by_uid uid =
+ let p = Proof_global.give_me_the_proof () in
+ let g = Goal.get_by_uid uid in
let pr gs =
- v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut ()
+ v 0 (str "goal / evar " ++ str uid ++ str " is:" ++ cut ()
++ pr_goal gs)
in
try
@@ -673,35 +682,10 @@ let pr_prim_rule = function
(str"cut " ++ pr_constr t ++
str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
- | FixRule (f,n,[],_) ->
- (str"fix " ++ pr_id f ++ str"/" ++ int n)
-
- | FixRule (f,n,others,j) ->
- if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
- let rec print_mut = function
- | (f,n,ar)::oth ->
- pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
- | [] -> mt () in
- (str"fix " ++ pr_id f ++ str"/" ++ int n ++
- str" with " ++ print_mut others)
-
- | Cofix (f,[],_) ->
- (str"cofix " ++ pr_id f)
-
- | Cofix (f,others,j) ->
- if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
- let rec print_mut = function
- | (f,ar)::oth ->
- (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
- | [] -> mt () in
- (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others)
| Refine c ->
str(if Termops.occur_meta c then "refine " else "exact ") ++
Constrextern.with_meta_as_hole pr_constr c
- | Thin ids ->
- (str"clear " ++ pr_sequence pr_id ids)
-
| Move (id1,id2) ->
(str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
@@ -713,10 +697,54 @@ let prterm = pr_lconstr
(* Printer function for sets of Assumptions.assumptions.
It is used primarily by the Print Assumptions command. *)
-open Assumptions
+type axiom =
+ | Constant of constant (* An axiom or a constant. *)
+ | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
+ | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
+
+type context_object =
+ | Variable of Id.t (* A section variable or a Let definition *)
+ | Axiom of axiom * (Label.t * Context.Rel.t * types) list
+ | Opaque of constant (* An opaque constant. *)
+ | Transparent of constant
+
+(* Defines a set of [assumption] *)
+module OrderedContextObject =
+struct
+ type t = context_object
+
+ let compare_axiom x y =
+ match x,y with
+ | Constant k1 , Constant k2 ->
+ con_ord k1 k2
+ | Positive m1 , Positive m2 ->
+ MutInd.CanOrd.compare m1 m2
+ | Guarded k1 , Guarded k2 ->
+ con_ord k1 k2
+ | _ , Constant _ -> 1
+ | _ , Positive _ -> 1
+ | _ -> -1
+
+ let compare x y =
+ match x , y with
+ | Variable i1 , Variable i2 -> Id.compare i1 i2
+ | Variable _ , _ -> -1
+ | _ , Variable _ -> 1
+ | Axiom (k1,_) , Axiom (k2, _) -> compare_axiom k1 k2
+ | Axiom _ , _ -> -1
+ | _ , Axiom _ -> 1
+ | Opaque k1 , Opaque k2 -> con_ord k1 k2
+ | Opaque _ , _ -> -1
+ | _ , Opaque _ -> 1
+ | Transparent k1 , Transparent k2 -> con_ord k1 k2
+end
+
+module ContextObjectSet = Set.Make (OrderedContextObject)
+module ContextObjectMap = Map.Make (OrderedContextObject)
let pr_assumptionset env s =
- if ContextObjectMap.is_empty s then
+ if ContextObjectMap.is_empty s &&
+ engagement env = (PredicativeSet, StratifiedType) then
str "Closed under the global context"
else
let safe_pr_constant env kn =
@@ -729,6 +757,12 @@ let pr_assumptionset env s =
try str " : " ++ pr_ltype typ
with e when Errors.noncritical e -> mt ()
in
+ let safe_pr_ltype_relctx (rctx, typ) =
+ let sigma, env = get_current_context () in
+ let env = Environ.push_rel_context rctx env in
+ try str " " ++ pr_ltype_env env sigma typ
+ with e when Errors.noncritical e -> mt ()
+ in
let pr_axiom env ax typ =
match ax with
| Constant kn ->
@@ -742,11 +776,19 @@ let pr_assumptionset env s =
let (v, a, o, tr) = accu in
match t with
| Variable id ->
- let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in
+ let var = pr_id id ++ str " : " ++ pr_ltype typ in
(var :: v, a, o, tr)
- | Axiom axiom ->
+ | Axiom (axiom, []) ->
let ax = pr_axiom env axiom typ in
(v, ax :: a, o, tr)
+ | Axiom (axiom,l) ->
+ let ax = pr_axiom env axiom typ ++
+ cut() ++
+ prlist_with_sep cut (fun (lbl, ctx, ty) ->
+ str " used in " ++ pr_label lbl ++
+ str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty))
+ l in
+ (v, ax :: a, o, tr)
| Opaque kn ->
let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
(v, a, opq :: o, tr)
@@ -757,6 +799,16 @@ let pr_assumptionset env s =
let (vars, axioms, opaque, trans) =
ContextObjectMap.fold fold s ([], [], [], [])
in
+ let theory =
+ if is_impredicative_set env then
+ [str "Set is impredicative"]
+ else []
+ in
+ let theory =
+ if type_in_type env then
+ str "Type hierarchy is collapsed (logic is inconsistent)" :: theory
+ else theory
+ in
let opt_list title = function
| [] -> None
| l ->
@@ -770,6 +822,7 @@ let pr_assumptionset env s =
opt_list (str "Section Variables:") vars;
opt_list (str "Axioms:") axioms;
opt_list (str "Opaque constants:") opaque;
+ opt_list (str "Theory:") theory;
] in
prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
@@ -782,3 +835,7 @@ let pr_polymorphic b =
if b then str"Polymorphic " else str"Monomorphic "
else mt ()
+let pr_universe_instance evd ctx =
+ let inst = Univ.UContext.instance ctx in
+ str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}"
+
diff --git a/printing/printer.mli b/printing/printer.mli
index a469a8dbed..695ab33b23 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -10,7 +10,6 @@ open Pp
open Names
open Globnames
open Term
-open Context
open Environ
open Pattern
open Evd
@@ -84,7 +83,8 @@ val pr_sort : evar_map -> sorts -> std_ppcmds
(** Universe constraints *)
val pr_polymorphic : bool -> std_ppcmds
-val pr_universe_ctx : Univ.universe_context -> std_ppcmds
+val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds
(** Printing global references using names as short as possible *)
@@ -108,13 +108,13 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds
val pr_context_unlimited : env -> evar_map -> std_ppcmds
val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds
-val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds
-val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds
-val pr_rel_decl : env -> evar_map -> rel_declaration -> std_ppcmds
+val pr_var_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
+val pr_var_list_decl : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds
+val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
-val pr_named_context : env -> evar_map -> named_context -> std_ppcmds
+val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds
val pr_named_context_of : env -> evar_map -> std_ppcmds
-val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds
+val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds
val pr_rel_context_of : env -> evar_map -> std_ppcmds
val pr_context_of : env -> evar_map -> std_ppcmds
@@ -160,12 +160,27 @@ val emacs_str : string -> string
val prterm : constr -> std_ppcmds (** = pr_lconstr *)
-(** spiwack: printer function for sets of Environ.assumption.
- It is used primarily by the Print Assumption command. *)
+(** Declarations for the "Print Assumption" command *)
+type axiom =
+ | Constant of constant (* An axiom or a constant. *)
+ | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
+ | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
+
+type context_object =
+ | Variable of Id.t (* A section variable or a Let definition *)
+ | Axiom of axiom * (Label.t * Context.Rel.t * types) list
+ | Opaque of constant (* An opaque constant. *)
+ | Transparent of constant
+
+module ContextObjectSet : Set.S with type elt = context_object
+module ContextObjectMap : CMap.ExtS
+ with type key = context_object and module Set := ContextObjectSet
+
val pr_assumptionset :
- env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds
+ env -> Term.types ContextObjectMap.t -> std_ppcmds
-val pr_goal_by_id : string -> std_ppcmds
+val pr_goal_by_id : Id.t -> std_ppcmds
+val pr_goal_by_uid : string -> std_ppcmds
type printer_pr = {
pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 652a34fa1f..bc8f0750e1 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -2,12 +2,8 @@ Genprint
Pputils
Ppannotation
Ppconstr
-Ppconstrsig
Printer
Pptactic
-Pptacticsig
Printmod
Prettyp
Ppvernac
-Ppvernacsig
-Richprinter
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 295d8aaa66..5f98eeeab9 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -65,17 +65,16 @@ let get_new_id locals id =
(** Inductive declarations *)
-open Termops
open Reduction
let print_params env sigma params =
if List.is_empty params then mt ()
else Printer.pr_rel_context env sigma params ++ brk(1,2)
-let print_constructors envpar names types =
+let print_constructors envpar sigma names types =
let pc =
prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
- (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c)
+ (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c)
(Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
in
hv 0 (str " " ++ pc)
@@ -83,21 +82,26 @@ let print_constructors envpar names types =
let build_ind_type env mip =
Inductive.type_of_inductive env mip
-let print_one_inductive env mib ((_,i) as ind) =
+let print_one_inductive env sigma mib ((_,i) as ind) =
let u = if mib.mind_polymorphic then
Univ.UContext.instance mib.mind_universes
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = extended_rel_list 0 params in
+ let args = Context.Rel.to_extended_list 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
let envpar = push_rel_context params env in
+ let inst =
+ if mib.mind_polymorphic then
+ Printer.pr_universe_instance sigma mib.mind_universes
+ else mt ()
+ in
hov 0 (
- pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++
- str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++
- brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
+ pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++
+ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
+ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
let print_mutual_inductive env mind mib =
let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
@@ -109,11 +113,13 @@ let print_mutual_inductive env mind mib =
| BiFinite -> "Variant"
| CoFinite -> "CoInductive"
in
+ let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
+ let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++
def keyword ++ spc () ++
prlist_with_sep (fun () -> fnl () ++ str" with ")
- (print_one_inductive env mib) inds ++
- Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+ (print_one_inductive env sigma mib) inds ++
+ Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
let get_fields =
let rec prodec_rec l subst c =
@@ -136,12 +142,14 @@ let print_record env mind mib =
in
let mip = mib.mind_packets.(0) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = extended_rel_list 0 params in
+ let args = Context.Rel.to_extended_list 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
let fields = get_fields cstrtype in
let envpar = push_rel_context params env in
+ let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in
+ let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
let keyword =
let open Decl_kinds in
match mib.mind_finite with
@@ -153,16 +161,16 @@ let print_record env mind mib =
hov 0 (
Printer.pr_polymorphic mib.mind_polymorphic ++
def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++
- print_params env Evd.empty params ++
- str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++
+ print_params env sigma params ++
+ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
str ":= " ++ pr_id mip.mind_consnames.(0)) ++
brk(1,2) ++
hv 2 (str "{ " ++
prlist_with_sep (fun () -> str ";" ++ brk(2,0))
(fun (id,b,c) ->
pr_id id ++ str (if b then " : " else " := ") ++
- Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++
- Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
+ Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
let pr_mutual_inductive_body env mind mib =
if mib.mind_record <> None && not !Flags.raw_print then
@@ -254,11 +262,16 @@ let nametab_register_modparam mbid mtb =
List.iter (nametab_register_body mp dir) struc
let print_body is_impl env mp (l,body) =
- let name = str (Label.to_string l) in
+ let name = pr_label l in
hov 2 (match body with
| SFBmodule _ -> keyword "Module" ++ spc () ++ name
| SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
| SFBconst cb ->
+ let u =
+ if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
+ else Univ.Instance.empty
+ in
+ let sigma = Evd.empty in
(match cb.const_body with
| Def _ -> def "Definition" ++ spc ()
| OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
@@ -267,15 +280,17 @@ let print_body is_impl env mp (l,body) =
| None -> mt ()
| Some env ->
str " :" ++ spc () ++
- hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *)
- (Typeops.type_of_constant_type env cb.const_type)) ++
+ hov 0 (Printer.pr_ltype_env env sigma
+ (Vars.subst_instance_constr u
+ (Typeops.type_of_constant_type env cb.const_type))) ++
(match cb.const_body with
| Def l when is_impl ->
spc () ++
hov 2 (str ":= " ++
- Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l))
+ Printer.pr_lconstr_env env sigma
+ (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
| _ -> mt ()) ++ str "." ++
- Printer.pr_universe_ctx cb.const_universes)
+ Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes))
| SFBmind mib ->
try
let env = Option.get env in
@@ -315,15 +330,17 @@ let rec print_typ_expr env mp locals mty =
let mapp = List.tl lapp in
hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
prlist_with_sep spc (print_modpath locals) mapp ++ str")")
- | MEwith(me,WithDef(idl,c))->
+ | MEwith(me,WithDef(idl,(c, _)))->
let env' = None in (* TODO: build a proper environment if env <> None *)
let s = String.concat "." (List.map Id.to_string idl) in
hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
- ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
- | MEwith(me,WithMod(idl,mp))->
+ ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
+ ++ Printer.pr_lconstr c)
+ | MEwith(me,WithMod(idl,mp'))->
let s = String.concat "." (List.map Id.to_string idl) in
hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++
- keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
+ keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
+ ++ print_modpath locals mp')
let print_mod_expr env mp locals = function
| MEident mp -> print_modpath locals mp
diff --git a/printing/printmod.mli b/printing/printmod.mli
index bea4753451..7f7d343927 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli
index 5d0d4ab0b4..f71fffdcec 100644
--- a/printing/printmodsig.mli
+++ b/printing/printmodsig.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
deleted file mode 100644
index d95e190749..0000000000
--- a/printing/richprinter.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-open Richpp
-
-module RichppConstr = Ppconstr.Richpp
-module RichppVernac = Ppvernac.Richpp
-module RichppTactic = Pptactic.Richpp
-
-type rich_pp =
- Ppannotation.t Richpp.located Xml_datatype.gxml
- * Xml_datatype.xml
-
-let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
-
-let make_richpp pr ast =
- let rich_pp =
- rich_pp get_annotations (pr ast)
- in
- let xml = Ppannotation.(
- xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
- )
- in
- (rich_pp, xml)
-
-let richpp_vernac = make_richpp RichppVernac.pr_vernac
-let richpp_constr = make_richpp RichppConstr.pr_constr_expr
-let richpp_tactic env = make_richpp (RichppTactic.pr_tactic env)
diff --git a/printing/richprinter.mli b/printing/richprinter.mli
deleted file mode 100644
index 41c313514b..0000000000
--- a/printing/richprinter.mli
+++ /dev/null
@@ -1,39 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** This module provides an entry point to "rich" pretty-printers that
- produce pretty-printing as done by {!Printer} but with additional
- annotations represented as a semi-structured document.
-
- To understand what are these annotations and how they are represented
- as standard XML attributes, please refer to {!Ppannotation}.
-
- In addition to these annotations, each node of the semi-structured
- document contains a [startpos] and an [endpos] attribute that
- relate this node to the raw pretty-printing.
- Please refer to {!Richpp} for more details. *)
-
-(** A rich pretty-print is composed of: *)
-type rich_pp =
-
- (** - a generalized semi-structured document whose attributes are
- annotations ; *)
- Ppannotation.t Richpp.located Xml_datatype.gxml
-
- (** - an XML document, representing annotations as usual textual
- XML attributes. *)
- * Xml_datatype.xml
-
-(** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *)
-val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp
-
-(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *)
-val richpp_constr : Constrexpr.constr_expr -> rich_pp
-
-(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *)
-val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 05:27:19 +0000