arithmetics for λδ

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / pnat_dis.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_dis.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_dis.ma
index cc226c94a682447f85becfd10a262808414f41d3..8c42f6f281cd8567ee8011f26c414e375a54da31 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_dis.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_dis.ma
@@ -14,7 +14,7 @@
 
 include "ground/arith/pnat.ma".
 
-(* POSITIVE INTEGERS ********************************************************)
+(* DISCRIMINATOR FOR POSITIVE INTEGERS **************************************)
 
 definition pdis (A:Type[0]) (a) (f) (p): A ≝
 match p with