diff options
| author | Hugo Herbelin | 2014-09-24 15:03:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-24 15:04:30 +0200 |
| commit | 9ec08ac299faf6acdfd6061fd21a00e3446aec79 (patch) | |
| tree | 2eed6d251673b4707696632380cd76d724136fff /printing/pptactic.ml | |
| parent | e24a118644d77e86ace11a34230711b204025c3b (diff) | |
Using an or_var rather than the hack with loc for coding a pure ident
as a disjunctive intropattern.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index bd4e9d93eb..9b27f9c7b4 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -377,8 +377,10 @@ let pr_bindings prc prlc = pr_bindings_gen false prc prlc let pr_with_bindings prc prlc (c,bl) = hov 1 (prc c ++ pr_bindings prc prlc bl) -let pr_as_disjunctive_ipat prc (_,ipatl) = - str "as " ++ Miscprint.pr_or_and_intro_pattern prc ipatl +let pr_as_disjunctive_ipat prc ipatl = + str "as " ++ + pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl + let pr_eqn_ipat (_,ipat) = str "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat let pr_with_induction_names prc = function |