From ead31bf3e2fe220d02dec59dce66471cc2c66fce Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 11 Aug 2003 10:25:04 +0000
Subject: Nouvelle mouture du traducteur v7->v8 Option -v8 à coqtop lance
 coqtopnew Le terminateur reste "." en v8 Ajout construction primitive
 CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les
 Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la
 traduction Ajout option -no-strict pour traduire les "Set Implicits" en
 implicites stricts + Bugs ou améliorations diverses Raffinement affichage
 projections de Record/Structure.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pattern.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping/pattern.ml')

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 92c581c719..d3479a8466 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -237,15 +237,16 @@ let rec pat_of_raw metas vars = function
       Options.if_verbose
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
-  | ROrderedCase (_,st,po,c,br) ->
+  | ROrderedCase (_,st,po,c,br,_) ->
       PCase ((None,st),option_app (pat_of_raw metas vars) po,
              pat_of_raw metas vars c,
              Array.map (pat_of_raw metas vars) br)
-  | RCases (loc,po,[c],brs) ->
+  | RCases (loc,(po,_),[c,_],brs) ->
       let sp =
 	match brs with
 	  | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
 	  | _ -> None in
+      (* When po disappears: switch to rtn type *)
       PCase ((sp,Term.RegularStyle),option_app (pat_of_raw metas vars) po,
              pat_of_raw metas vars c,
              Array.init (List.length brs)
-- 
cgit v1.2.3