diff options
| author | msozeau | 2008-01-31 15:19:22 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-31 15:19:22 +0000 |
| commit | 7f99d8016ced351efd0a42598a9d18001b2e4d46 (patch) | |
| tree | db617f28100f0b621743d810851eadd1eac3720e /pretyping | |
| parent | 2b9f73c7e86ac718c0ce4c47d6a24ffc2d01499d (diff) | |
Finish let| implementation and document it
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10489 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 9 |
2 files changed, 12 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index f0203fa2c4..b6ec169254 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -321,6 +321,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = try if !Flags.raw_print then RegularStyle + else if st = LetPatternStyle then + st else if PrintingLet.active (indsp,consnargsl) then LetStyle else if PrintingIf.active (indsp,consnargsl) then @@ -334,6 +336,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let bl' = Array.map detype bl in let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in RLetTuple (dl,nal,(alias,pred),tomatch,d) + | LetPatternStyle when List.length eqnl = 1 -> (* If irrefutable due to some inversion, print as match *) + RLetPattern (dl,(tomatch,(alias,aliastyp)),List.hd eqnl) | IfStyle when aliastyp = None -> let bl' = Array.map detype bl in let nondepbrs = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index db492c026b..e30f553fe0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -588,7 +588,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct let j = pretype tycon env evdref lvar (RCases (loc, None, [c], [p])) - in j + in + (* Change case info *) + let j' = match kind_of_term j.uj_val with + Case (ci, po, c, br) -> + let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in + { j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) } + | _ -> j + in j' | RCases (loc,po,tml,eqns) -> Cases.compile_cases loc |