aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-18 17:30:09 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-21 19:36:38 +0100
commit589130e87d68227d25800e7506666eaf1d47a25a (patch)
treeff7ae021ca3c3306bbcbc8b9575b3b23b78320ce /printing
parent329b5b9ed526d572d7df066dc99486e1dcb9e4cc (diff)
Changing the toplevel type of the int_or_var generic type to int.
Diffstat (limited to 'printing')
-rw-r--r--printing/pptactic.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index b51130075..94cbc54e9 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -337,7 +337,7 @@ module Make
let rec pr_top_generic_rec prc prlc prtac prpat x =
match Genarg.genarg_tag x with
- | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
+ | IntOrVarArgType -> int (out_gen (topwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
| VarArgType -> pr_id (out_gen (topwit wit_var) x)
| ConstrArgType -> prc (out_gen (topwit wit_constr) x)