diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 3d1e3e054..5356cdee8 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -366,7 +366,6 @@ module Make in str "<" ++ name ++ str ">" ++ args - let pr_alias_key key = try let prods = (KNmap.find key !prnotation_tab).pptac_prods in @@ -383,7 +382,7 @@ module Make str (String.concat " " (pr prods)) with Not_found -> KerName.print key - + let pr_alias_gen pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in |