diff options
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 254a789c0..f354ac44f 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -261,8 +261,6 @@ let rec pr_tacarg_using_rule pr_gen = function | [], [] -> mt () | _ -> failwith "Inconsistent arguments of extended tactic" -let surround p = hov 1 (str"(" ++ p ++ str")") - let pr_extend_gen prgen lev s l = try let tags = List.map genarg_tag l in |