Did that adding a rule for printing applications as "f(x)" works.

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

2 files changed, 30 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fa0e189153..08db24dbaa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -747,16 +747,22 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
       try
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args,argsscopes,argsimpls) = match t,n with
-	  | GApp (_,(GRef (_,ref) as f),args), Some n
+	  | GApp (_,f,args), Some n
 	      when List.length args >= n ->
 	      let args1, args2 = list_chop n args in
-	      let subscopes =
-		try list_skipn n (find_arguments_scope ref) with _ -> [] in
-	      let impls =
-		let impls =
-		  select_impargs_size
-		    (List.length args) (implicits_of_global ref) in
-		try list_skipn n impls with _ -> [] in
+              let subscopes, impls =
+                match f with
+                | GRef (_,ref) ->
+	          let subscopes =
+		    try list_skipn n (find_arguments_scope ref) with _ -> [] in
+	          let impls =
+		    let impls =
+		      select_impargs_size
+		        (List.length args) (implicits_of_global ref) in
+		    try list_skipn n impls with _ -> [] in
+                  subscopes,impls
+                | _ ->
+                  [], [] in
 	      (if n = 0 then f else GApp (dummy_loc,f,args1)),
 	      args2, subscopes, impls
 	  | GApp (_,(GRef (_,ref) as f),args), None ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 771e856921..ae14cd5ca9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -187,11 +187,15 @@ type key =
 let notations_key_table = ref Gmapl.empty
 let prim_token_key_table = Hashtbl.create 7
 
-let glob_constr_key = function
-  | GApp (_,GRef (_,ref),_) -> RefKey (canonical_gr ref)
-  | GRef (_,ref) -> RefKey (canonical_gr ref)
+let glob_prim_constr_key = function
+  | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref)
   | _ -> Oth
 
+let glob_constr_keys = function
+  | GApp (_,GRef (_,ref),_) -> [RefKey (canonical_gr ref); Oth]
+  | GRef (_,ref) -> [RefKey (canonical_gr ref)]
+  | _ -> [Oth]
+
 let cases_pattern_key = function
   | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
   | _ -> Oth
@@ -201,6 +205,7 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
   | AList (_,_,AApp (ARef ref,args),_,_)
   | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
   | ARef ref -> RefKey(canonical_gr ref), None
+  | AApp (_,args) -> Oth, Some (List.length args)
   | _ -> Oth, None
 
 (**********************************************************************)
@@ -234,7 +239,8 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
   declare_scope sc;
   add_prim_token_interpreter sc interp;
   List.iter (fun pat ->
-      Hashtbl.add prim_token_key_table (glob_constr_key pat) (sc,uninterp,b))
+      Hashtbl.add prim_token_key_table
+        (glob_prim_constr_key pat) (sc,uninterp,b))
     patl
 
 let mkNumeral n = Numeral n
@@ -369,8 +375,11 @@ let rec interp_notation loc ntn local_scopes =
     user_err_loc
     (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
 
+let isGApp = function GApp _ -> true | _ -> false
+
 let uninterp_notations c =
-  Gmapl.find (glob_constr_key c) !notations_key_table
+  list_map_append (fun key -> Gmapl.find key !notations_key_table)
+    (glob_constr_keys c)
 
 let uninterp_cases_pattern_notations c =
   Gmapl.find (cases_pattern_key c) !notations_key_table
@@ -382,7 +391,8 @@ let availability_of_notation (ntn_scope,ntn) scopes =
 
 let uninterp_prim_token c =
   try
-    let (sc,numpr,_) = Hashtbl.find prim_token_key_table (glob_constr_key c) in
+    let (sc,numpr,_) =
+      Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in
     match numpr c with
       | None -> raise No_match
       | Some n -> (sc,n)