diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-17 20:32:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-17 20:32:53 +0100 |
| commit | 0b6433c9b1de1a5726e29ca2268f9a2c6d8a2667 (patch) | |
| tree | a158fb504839df633235ecc2b29042551fef9958 /printing/ppconstr.ml | |
| parent | 10e54c76b72ab545552fbd5e50aa07993a3c703a (diff) | |
Fixing semantics of Ppconstr.print_hunks.
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 466cd8444..e9fddd815 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -72,7 +72,7 @@ end) = struct let print_hunks n pr pr_binders (terms, termlists, binders) unps = let env = ref terms and envlist = ref termlists and bll = ref binders in let pop r = let a = List.hd !r in r := List.tl !r; a in - let return unp pp1 pp2 = tag_unparsing unp (pp1 ++ pp2) in + let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in (* Warning: The following function enforces a very precise order of evaluation of sub-components. |