diff options
Diffstat (limited to 'plugins/decl_mode/ppdecl_proof.ml')
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 102da8cc..27308666 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <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 *) (************************************************************************) -open Util +open Errors open Pp open Decl_expr open Names @@ -20,6 +20,8 @@ let pr_label = function Anonymous -> mt () | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () +let pr_constr env c = pr_constr env Evd.empty c + let pr_justification_items env = function Some [] -> mt () | Some (_::_ as l) -> @@ -75,7 +77,7 @@ and print_vars pconstr gtyp env sep _be _have vars = begin let nenv = match st.st_label with - Anonymous -> anomaly "anonymous variable" + Anonymous -> anomaly (Pp.str "anonymous variable") | Name id -> Environ.push_named (id,None,st.st_it) env in let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ @@ -173,14 +175,14 @@ let rec pr_bare_proof_instr _then _thus env = function str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ pr_casee env c | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et - | _ -> anomaly "unprintable instruction" + | _ -> anomaly (Pp.str "unprintable instruction") let pr_emph = function 0 -> str " " | 1 -> str "* " | 2 -> str "** " | 3 -> str "*** " - | _ -> anomaly "unknown emphasis" + | _ -> anomaly (Pp.str "unknown emphasis") let pr_proof_instr env instr = pr_emph instr.emph ++ spc () ++ |