From 7e035682056388e730f03e214774d093e06ef650 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 14 Oct 2009 12:52:06 +0000 Subject: [PATCH] minor fix --- helm/software/matita/nlibrary/topology/igft.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2