diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 20:35:19 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:36 +0100 |
| commit | 830321178ad0b71aea92b1fabaeaa208601ea9ae (patch) | |
| tree | 15f95ed365e47d40bc0cac4e019f6d532511f05b /printing | |
| parent | 678b17b52b0b59a5470d8272474e692b2fe023e3 (diff) | |
Rebase artefact.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7420f2784..315301d93 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1222,7 +1222,6 @@ module Make return (keyword "BeginSubproof" ++ spc () ++ int i) | VernacEndSubproof -> return (str "}") ->>>>>>> Ppannotation.t: New constructor AVernac. and pr_vernac_list l = hov 2 (str"[" ++ spc() ++ |