aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml2
-rw-r--r--printing/genprint.mli2
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--printing/ppconstr.mli2
-rw-r--r--printing/pputils.ml2
-rw-r--r--printing/pputils.mli2
-rw-r--r--printing/prettyp.ml14
-rw-r--r--printing/prettyp.mli2
-rw-r--r--printing/printer.ml18
-rw-r--r--printing/printer.mli4
-rw-r--r--printing/printmod.ml4
-rw-r--r--printing/printmod.mli2
-rw-r--r--printing/proof_diffs.ml2
-rw-r--r--printing/proof_diffs.mli2
14 files changed, 40 insertions, 20 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 2f0f7f48c9..a04df31d30 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 24b008643b..21b8417ffa 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 27ed2189ed..aea4f23205 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 219fe4336a..c17ca251a8 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index fff6dae1b4..5ec2f93cd8 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/printing/pputils.mli b/printing/pputils.mli
index d0f3e61eac..f260c4a373 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f55bfb504f..a2bdb30773 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -583,11 +583,15 @@ let print_constant with_values sep sp udecl =
str"*** [ " ++
print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
str" ]" ++
- Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs
- | Some (c, ctx) ->
+ Printer.pr_universes sigma univs
+ | Some (c, priv, ctx) ->
+ let priv = match priv with
+ | Opaqueproof.PrivateMonomorphic () -> None
+ | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx
+ in
print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
- Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs)
+ Printer.pr_universes sigma univs ?priv)
let gallina_print_constant_with_infos sp udecl =
print_constant true " = " sp udecl ++
@@ -723,7 +727,7 @@ let print_full_pure_context env sigma =
| OpaqueDef lc ->
str "Theorem " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
- str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc)
+ str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc))
| Def c ->
str "Definition " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 9213bc8561..7485f4bd19 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/printing/printer.ml b/printing/printer.ml
index 2951d8e5c8..1f68018678 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -831,6 +831,22 @@ let pr_goal_by_id ~proof id =
pr_selected_subgoal (pr_id id) sigma g)
with Not_found -> user_err Pp.(str "No such goal.")
+(** print a goal identified by the goal id as it appears in -emacs mode.
+ sid should be the Stm state id corresponding to proof. Used to support
+ the Prooftree tool in Proof General. (https://askra.de/software/prooftree/).
+*)
+let pr_goal_emacs ~proof gid sid =
+ match proof with
+ | None -> user_err Pp.(str "No proof for that state.")
+ | Some proof ->
+ let pr gs =
+ v 0 ((str "goal ID " ++ (int gid) ++ str " at state " ++ (int sid)) ++ cut ()
+ ++ pr_goal gs)
+ in
+ try
+ Proof.in_proof proof (fun sigma -> pr {it=(Evar.unsafe_of_int gid);sigma=sigma;})
+ with Not_found -> user_err Pp.(str "No such goal.")
+
(* Printer function for sets of Assumptions.assumptions.
It is used primarily by the Print Assumptions command. *)
diff --git a/printing/printer.mli b/printing/printer.mli
index 4e27268c4d..a72f319636 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -206,4 +206,4 @@ module ContextObjectMap : CMap.ExtS
val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
-
+val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t
diff --git a/printing/printmod.ml b/printing/printmod.ml
index bd97104f60..74d4f69c9c 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -297,7 +297,7 @@ let print_body is_impl extent env mp (l,body) =
hov 2 (str ":= " ++
Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
| _ -> mt ()) ++ str "." ++
- Printer.pr_abstract_universe_ctx sigma ctx ?priv:cb.const_private_poly_univs)
+ Printer.pr_abstract_universe_ctx sigma ctx)
| SFBmind mib ->
match extent with
| WithContents ->
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 48ba866cc0..8fd1cb4183 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index abb0d55b39..233163d097 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index fd10eaa458..f6fca91eea 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:38:38 +0000