minor fix

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 96f419aa33ebf03269bd40264dd2edd825b866bc..e98696589e2f30f48fdfa9011a8df7c1c2692285 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -366,7 +366,7 @@ of the inductive predicate) on the right of `:`.
 
 D*)
 
-(* ncheck xcreflexivity. *)
+(** ncheck xcreflexivity. *) (* shows: ∀A:Ax.∀U:Ω^A.∀a:A.a∈U → xcover A U a *)
 
 (*D
 
@@ -544,7 +544,7 @@ but not introduction rules for the coinductive case.
 
 D*)
 
-(* ncheck cover_rect_CProp0. *) 
+(** ncheck cover_rect_CProp0. *) 
 
 (*D