From 7f99d8016ced351efd0a42598a9d18001b2e4d46 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 31 Jan 2008 15:19:22 +0000
Subject: Finish let| implementation and document it

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10489 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/detyping.ml  | 4 ++++
 pretyping/pretyping.ml | 9 ++++++++-
 2 files changed, 12 insertions(+), 1 deletion(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3