From a982d8d4f17ab876ad03658a71fa4b964d8ccd3b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Dec 2005 15:53:14 +0000 Subject: [PATCH] since the moo content is not OK... we need an hack. --- helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma index acbc2ecf1..47fd8ab61 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma @@ -16,7 +16,10 @@ set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_props". include "coa_defs.ma". -theorem zero_le: \forall (P:COA). \forall (p:Type_of_COA P). le ? (zero P) p. +coercion Type_of_COA. (* this should be generated by the following line *) +coercion coa. (* this should be inside coa_defs.moo but it isn't *) + +theorem zero_le: \forall (P:COA). \forall (p:P). le ? (zero P) p. -- 2.39.2