aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness/ptyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/correctness/ptyping.ml')
-rw-r--r--contrib/correctness/ptyping.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index 2e95f840f..a6f7a0ae9 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -529,7 +529,7 @@ let rec states_desc ren env loc = function
if s_e.info.kappa = c then
s_e
else begin
- if !verbose_fix then begin mSGNL (pp_type_c s_e.info.kappa) end ;
+ if !verbose_fix then begin msgnl (pp_type_c s_e.info.kappa) end ;
state_rec s_e.info.kappa
end
in