aboutsummaryrefslogtreecommitdiff
path: root/parsing/pptactic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pptactic.ml')
-rw-r--r--parsing/pptactic.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2f86ac94cf..f18bcf414a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -127,7 +127,7 @@ let rec pr_message_token prid = function
| MsgInt n -> int n
| MsgIdent id -> prid id
-let rec pr_raw_generic prc prlc prtac prref x =
+let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) Genarg.generic_argument) =
match Genarg.genarg_tag x with
| BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
| IntArgType -> pr_arg int (out_gen rawwit_int x)