From 33c0d3b95bdf0ff1fdd2d6dbe7088e48c2fa6f67 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sat, 7 Nov 2015 16:01:27 +0100
Subject: GRAMMAR: added punctuation

---
 doc/refman/RefMan-cic.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 2a4ccfed87..092dba46b4 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1738,7 +1738,7 @@ The first stage is to precise on which argument the fixpoint will be
 decreasing. The type of this argument should be an inductive
 definition.
 
-For doing this the syntax of fixpoints is extended and becomes 
+For doing this, the syntax of fixpoints is extended and becomes 
  \[\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}\]
 where $k_i$ are positive integers.
 Each $A_i$ should be a type (reducible to a term) starting with at least
-- 
cgit v1.2.3