From 69ed6089d7ed778e37f5442f57ef7693f73ca802 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 26 Apr 2016 06:06:17 +0200
Subject: Fixing a mispelling coma -> comma.

---
 plugins/funind/g_indfun.ml4 | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index aa9cc40234..893baad8c9 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -123,12 +123,12 @@ TACTIC EXTEND snewfunind
 END
 
 
-let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc
+let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc
 
-ARGUMENT EXTEND constr_coma_sequence'
+ARGUMENT EXTEND constr_comma_sequence'
   TYPED AS constr_list
-  PRINTED BY pr_constr_coma_sequence
-| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ]
+  PRINTED BY pr_constr_comma_sequence
+| [ constr(c) "," constr_comma_sequence'(l) ] -> [ c::l ]
 | [ constr(c) ] -> [ [c] ]
 END
 
@@ -137,7 +137,7 @@ let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
 ARGUMENT EXTEND auto_using'
   TYPED AS constr_list
   PRINTED BY pr_auto_using
-| [ "using" constr_coma_sequence'(l) ] -> [ l ]
+| [ "using" constr_comma_sequence'(l) ] -> [ l ]
 | [ ] -> [ [] ]
 END
 
-- 
cgit v1.2.3