diff options
| author | Pierre-Marie Pédrot | 2016-05-08 18:59:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-08 19:59:03 +0200 |
| commit | f461e7657cab9917c5b405427ddba3d56f197efb (patch) | |
| tree | 467ac699f78d0360b05174238aeb1177da892503 /printing/ppvernac.ml | |
| parent | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff) | |
Removing dead code and unused opens.
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f0548238a7..10b2bda05e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -99,11 +99,6 @@ module Make | ETBinder false -> str "closed binder" | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" - let strip_meta id = - let s = Id.to_string id in - if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1)) - else id - let pr_comment pr_c = function | CommentConstr c -> pr_c c | CommentString s -> qs s |