diff options
| author | Hugo Herbelin | 2014-09-11 20:00:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-12 10:39:32 +0200 |
| commit | ca300977724a6b065a98c025d400c71f41b9df4b (patch) | |
| tree | 59a2fd3327b3d0eb9cd1e11cbb31605f2a08ea27 /printing/ppconstr.ml | |
| parent | 012fe1a96ba81ab0a7fa210610e3f25187baaf1d (diff) | |
Parsing evar instances.
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 6956ec4481..baafbc04fd 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -177,8 +177,8 @@ let pr_prim_token = function let pr_evar pr id l = hov 0 (str "?" ++ pr_id id ++ (match l with - | None | Some [] -> mt() - | Some l -> + | [] -> mt() + | l -> let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in str"@{" ++ hov 0 (prlist_with_sep pr_comma f l) ++ str"}")) @@ -554,7 +554,7 @@ let pr pr sep inherited a = | CHole _ -> str "_", latom | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom - | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom + | CPatVar (_,p) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_glob_sort s, latom | CCast (_,a,b) -> hv 0 (pr mt (lcast,L) a ++ cut () ++ |