diff options
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 597505686d..cf5a58eea4 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -122,6 +122,7 @@ let pr_rawsort = function let pr_id = pr_id let pr_name = pr_name let pr_qualid = pr_qualid +let pr_patvar = pr_id let pr_expl_args pr (a,expl) = match expl with |