ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_proof_checking / doc / inductive.txt

diff --git a/helm/ocaml/cic_proof_checking/doc/inductive.txt b/helm/ocaml/cic_proof_checking/doc/inductive.txt
index 4cc9cade63223e35908d996a7aa7573dee4d0d41..f2e49d3987fb770d9d3e940dd4094583f41f9aca 100644 (file)
--- 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)