aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-04-02 11:20:21 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-04-02 11:20:21 +0200
commit3fe764dd8d6578adddb01b02bafc7f31d9cb776c (patch)
tree903b49e6df3e92730b19193bb54b71383f7155fa /printing/ppconstr.ml
parentc68dc1748febb49f8eae7fc06794aa262c95a382 (diff)
Fix higher-order pattern variables not being printed as "@?" (bug #5431).
Diffstat (limited to 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d92d83275..7f5adbfe4 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -703,7 +703,7 @@ let tag_var = tag Tag.variable
| CEvar (_,n,l) ->
return (pr_evar (pr mt) n l, latom)
| CPatVar (_,p) ->
- return (str "?" ++ pr_patvar p, latom)
+ return (str "@?" ++ pr_patvar p, latom)
| CSort (_,s) ->
return (pr_glob_sort s, latom)
| CCast (_,a,b) ->