X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2Fdoc%2Finductive.txt;h=f2e49d3987fb770d9d3e940dd4094583f41f9aca;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4cc9cade63223e35908d996a7aa7573dee4d0d41;hpb=aaf75c2cff13515b049a15cc8a96734e8967ae9b;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/doc/inductive.txt b/helm/ocaml/cic_proof_checking/doc/inductive.txt
index 4cc9cade6..f2e49d398 100644
--- a/helm/ocaml/cic_proof_checking/doc/inductive.txt
+++ b/helm/ocaml/cic_proof_checking/doc/inductive.txt
@@ -36,5 +36,6 @@ Legenda:
   non-informative : Constructor arguments are in Prop only
   small : Constructor arguments are not in Type and SetP and CProp
   unit : Non (mutually) recursive /\ only one constructor /\ non-informative
-  empty : no contructors and (in Coq) non mutually recursive
-            
+  empty : in Coq:    no constructors and non mutually recursive
+          in Matita: no constructors (but eventually mutually recursive
+                     with non-empty types)