diff options
Diffstat (limited to 'plugins/decl_mode/ppdecl_proof.ml')
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 7f63c4200..be2e44cff 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -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) -> |