aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/showproof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/showproof.ml')
-rw-r--r--contrib/interface/showproof.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 5bfad2f52..c23394e8c 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1806,7 +1806,7 @@ let show_proof lang gpath =
;;
let show_nproof path =
- pP (sp_print (sph [spi; show_proof "fr" path]));;
+ pp (sp_print (sph [spi; show_proof "fr" path]));;
vinterp_add "ShowNaturalProof"
(fun _ ->