diff options
| author | Pierre-Marie Pédrot | 2016-05-04 14:30:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-04 14:34:18 +0200 |
| commit | 8d3f0b614d7b2fb30f6e87b48a4fc5c0d286e49c (patch) | |
| tree | 6a244976f5caef6a2b88c84053fce87f94c78f96 /printing/pptactic.ml | |
| parent | c7fd62135403c1ea38194fcdd8035237ee108318 (diff) | |
Normalizing the names of dynamic types to follow a typ_* scheme.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 6fb68ddf42..9ab6895f3b 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -108,12 +108,12 @@ module Make | Some Refl -> x let rec pr_value lev v : std_ppcmds = - if has_type v Val.list_tag then - pr_sequence (fun x -> pr_value lev x) (unbox v Val.list_tag) - else if has_type v Val.opt_tag then - pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.opt_tag) - else if has_type v Val.pair_tag then - let (v1, v2) = unbox v Val.pair_tag in + if has_type v Val.typ_list then + pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list) + else if has_type v Val.typ_opt then + pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt) + else if has_type v Val.typ_pair then + let (v1, v2) = unbox v Val.typ_pair in str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")" else let Val.Dyn (tag, x) = v in |