Syntaxe plus liberale pour le type des arguments de filtrage du 'match'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 2 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 5e5a3236b4..51b2a69535 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -336,7 +336,13 @@ let is_var id = function
   | _ -> false
 
 let tm_clash = function
-  | (CRef (Ident (_,id)), Some (_,_,nal)) when List.exists ((=) (Name id)) nal
+  | (CRef (Ident (_,id)), Some (CApp (_,_,nal))) 
+      when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false)
+	nal
+      -> Some id
+  | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal))) 
+      when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false)
+	nal
       -> Some id
   | _ -> None
 
@@ -350,9 +356,12 @@ let pr_case_item pr (tm,(na,indnalopt)) =
     | _ -> mt ()) ++
   (match indnalopt with
     | None -> mt ()
+(*
     | Some (_,ind,nal) ->
         spc () ++ str "in " ++ 
-        hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal)))
+        hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal))
+*)
+    | Some t -> spc () ++ str "in " ++ pr lsimple t))
 
 let pr_case_type pr po =
   match po with