diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
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 |