From 899b701462fa056a22f997ae22c5ef7c1d247673 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2015 21:01:29 +0200
Subject: Starting revising inductive types session

---
 doc/refman/RefMan-cic.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 8e1a1766e5..5002b905c7 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -534,11 +534,11 @@ reductions or any combination of those can also be defined.
 \section[Inductive Definitions]{Inductive Definitions\label{Cic-inductive-definitions}}
 
 A (possibly mutual) inductive definition is specified by giving the
-names and the type of the inductive sets or families to be
-defined and the names and types of the constructors of the inductive
-predicates.  An inductive declaration in the global environment can
-consequently be represented with two local contexts (one for inductive
-definitions, one for constructors).
+names and types of the inductive types to be
+defined and the names and types of the constructors of the inductive types.
+An inductive declaration in the global environment can
+consequently be represented with two local contexts, one for the types
+one for the constructors.
 
 Stating the rules for inductive definitions in their general form
 needs quite tedious definitions. We shall try to give a concrete
-- 
cgit v1.2.3