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
---
 contrib/subtac/subtac_pretyping_F.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 986825f25c..9669acc230 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -493,7 +493,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let j = 
 	  pretype tycon env isevars lvar 
 	    (RCases (loc, None, [c], [p]))
-	in j
+	(* 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