From 3d954bd02e4e56f7aa973230db519adde18d8e12 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 26 May 2005 16:27:30 +0000
Subject: No parentheses around f in 'f \subst{...}'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7083 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/whelp.ml4 | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index dfda566230..292eb0c3f3 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -114,9 +114,12 @@ let merge vl al =
   in aux [] (vl,al)
 
 let rec uri_of_constr c =
-  url_paren (fun () -> match c with
+  match c with
   | RVar (_,id) -> url_id id
   | RRef (_,ref) ->  uri_of_global ref
+  | RHole _ | REvar _ -> url_string "?"
+  | RSort (_,s) -> url_string (whelp_of_rawsort s)
+  | _ -> url_paren (fun () -> match c with
   | RApp (_,f,args) ->
       let inst,rest = merge (section_parameters f) args in
       uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; 
@@ -134,10 +137,10 @@ let rec uri_of_constr c =
       uri_of_constr b; url_string " in "; uri_of_constr c
   | RCast (_,c,t) ->
       uri_of_constr c; url_string ":"; uri_of_constr t
-  | RHole _ | REvar _ -> url_string "?"
-  | RSort (_,s) -> url_string (whelp_of_rawsort s)
   | RRec _ | RIf _ | RLetTuple _ | ROrderedCase _ | RCases _ ->
       error "Whelp does not support pattern-matching and (co-)fixpoint"
+  | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ ->
+      anomaly "Written w/o parenthesis"
   | RPatVar _ | RDynamic _ -> 
       anomaly "Found constructors not supported in constr") ()
 
-- 
cgit v1.2.3