aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/extraargs.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index c3377bca1f..4a6c2ffb25 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -279,6 +279,7 @@ let pr_r_int31_field _ _ _ i31f =
| Retroknowledge.Int31PhiInv -> str "phi inv"
| Retroknowledge.Int31Plus -> str "plus"
| Retroknowledge.Int31Times -> str "times"
+ | _ -> assert false
let pr_retroknowledge_field _ _ _ f =
match f with