From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 14 Oct 2009 12:52:06 +0000 (+0000)
Subject: minor fix
X-Git-Tag: make_still_working~3306
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e035682056388e730f03e214774d093e06ef650;hp=fe0042aeb03b19271cd61f402a44ec23e3100ea7;p=helm.git

minor fix
---

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 96f419aa3..e98696589 100644
--- 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