From a885a2148e4d45606c654145db5d859c4d6a223b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 12 Jun 2010 15:30:28 +0000
Subject: Fixing spelling: pr_coma -> pr_comma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/g_indfun.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 81c7c29d22..fc8f7ac966 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -112,7 +112,7 @@ TACTIC EXTEND snewfunind
 END
 
 
-let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc
+let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_comma prc
 
 ARGUMENT EXTEND constr_coma_sequence'
   TYPED AS constr_list
-- 
cgit v1.2.3