removed spurious CVSROOT from the old repository

[helm.git] / helm / matita / contribs / PREDICATIVE-TOPOLOGY / domain_defs.ma

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
index 670211caf3cee1f047c44187a6f222f9fbc13ae6..68cbd01fa8d962b3d0a829959f45266dfbb971f0 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
@@ -24,38 +24,35 @@ include "class_defs.ma".
 *)
 
 record Domain: Type \def {
-   qd: Class
+   qd:> Class
 }.
 
-coercion qd.
-
 (* internal universal quantification *)
-inductive iall (D:Domain) (P:D \to Prop) : Prop \def
-   | iall_intro: (\forall d:D. cin D d \to P d) \to iall D P.
+inductive dall (D:Domain) (P:D \to Prop) : Prop \def
+   | dall_intro: (\forall d:D. cin D d \to P d) \to dall D P.
 
 (* internal existential quantification *)
-inductive iex (D:Domain) (P:D \to Prop) : Prop \def
-   | iex_intro: \forall d:D. cin D d \land P d \to iex D P.
-(*
+inductive dex (D:Domain) (P:D \to Prop) : Prop \def
+   | dex_intro: \forall d:D. cin D d \land P d \to dex D P.
+
 (* notations **************************************************************)
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "internal for all" 'iall \eta.x =
-  (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/iall.ind#xpointer(1/1) _ x).
+interpretation "internal for all" 'iforall \eta.x =
+  (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dall.ind#xpointer(1/1) _ x).
 
-notation < "hvbox(\iall ident i opt (: ty) break . p)"
+notation > "hvbox(\iforall ident i opt (: ty) break . p)"
   right associative with precedence 20
-for @{ 'iall ${default
+for @{ 'iforall ${default
   @{\lambda ${ident i} : $ty. $p)}
   @{\lambda ${ident i} . $p}}}.
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "internal exist" 'iexist \eta.x =
-  (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/iex.ind#xpointer(1/1) _ x).
+interpretation "internal exists" 'dexists \eta.x =
+  (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dex.ind#xpointer(1/1) _ x).
 
-notation < "hvbox(\iexist ident i opt (: ty) break . p)"
+notation > "hvbox(\iexists ident i opt (: ty) break . p)"
   right associative with precedence 20
-for @{ 'iexist ${default
+for @{ 'dexists ${default
   @{\lambda ${ident i} : $ty. $p)}
   @{\lambda ${ident i} . $p}}}.
-*)
\ No newline at end of file