From f35b7d420a31d98c82a4ee3bef631c9fa1b846f9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 20 Mar 2007 17:33:35 +0000
Subject: Correction bug affichage des notations des noms de fonctions
 appliquées

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9723 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4fbf57e07a..d5de74f8ab 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -830,7 +830,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 	let (t,args) = match t,n with
 	  | RApp (_,f,args), Some n when List.length args > n ->
 	      let args1, args2 = list_chop n args in
-	      RApp (dummy_loc,f,args1), args2
+	      (if n = 0 then f else RApp (dummy_loc,f,args1)), args2
 	  | _ -> t,[] in
 	(* Try matching ... *)
 	let subst = match_aconstr t pat in
-- 
cgit v1.2.3