update in basic_2 and apps_2

[helm.git] / helm / software / matita / contribs / limits / Domain / defs.ma

diff --git a/helm/software/matita/contribs/limits/Domain/defs.ma b/helm/software/matita/contribs/limits/Domain/defs.ma
index f73f1aca0458710a25cce24b08a0bfe675c67f33..f828ff1ae60060365342df0210cdcf82069fe5fe 100644 (file)
--- a/helm/software/matita/contribs/limits/Domain/defs.ma
+++ b/helm/software/matita/contribs/limits/Domain/defs.ma
@@ -28,11 +28,11 @@ inductive dall (D:Domain) (P:D → Prop): Prop ≝
    | dall_intro: (∀d. cin ? d → P d) → dall D P
 .
 
-interpretation "internal for all" 'iforall η.x = (dall _ x).
+interpretation "internal for all" 'iforall η.x = (dall ? x).
 
 (* internal existential quantification *)
 inductive dex (D:Domain) (P:D → Prop): Prop ≝
    | dex_intro: ∀d. cin D d → P d → dex D P
 .
 
-interpretation "internal exists" 'iexists η.x = (dex _ x).
+interpretation "internal exists" 'iexists η.x = (dex ? x).