coercion command now requires an uri

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
index ba119561956e16c043898fe57df069a1530385a6..acd73c4ba686ca00ca9523bfd27130bc730df00a 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
@@ -37,13 +37,11 @@ definition true_f \def \lambda (X:Type). \lambda (_:X). True.
 definition false_f \def \lambda (X:Type). \lambda (_:X). False.
 
 record Class: Type \def {
-   class: Type;
+   class:> Type;
    cin  : class \to Prop;
    cle1 : class \to class \to Prop
 }.
 
-coercion class. 
-
 inductive ceq (C:Class) (c1:C): C \to Prop \def
    | ceq_refl:   cin ? c1 \to ceq ? c1 c1
    | ceq_sing_r: \forall c2,c3. 

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
index 916c91cd80f0db43d9d7db18c242529a7c46a0bd..68cbd01fa8d962b3d0a829959f45266dfbb971f0 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
@@ -24,11 +24,9 @@ include "class_defs.ma".
 *)
 
 record Domain: Type \def {
-   qd: Class
+   qd:> Class
 }.
 
-coercion qd.
-
 (* internal universal quantification *)
 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.

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
index 3cc583f02db26d1a44d1baec206424478c616dab..cf981362c42f6808286f2417cac0869117c6f172 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
@@ -60,7 +60,7 @@ definition domain_of_subset: \forall D. (Subset D) \to Domain \def
    \lambda (D:Domain). \lambda U. 
    mk_Domain (mk_Class D (sin D U) (cle1 D)).
 
-coercion domain_of_subset.   
+coercion cic:/matita/PREDICATIVE-TOPOLOGY/subset_defs/domain_of_subset.con.
 
 (* the full subset of a domain *)
 coercion stop.

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index d18c80b23ac323b996280a835a52912fc2ffc8ce..ea50a2cd9c3b70729df6c8c6bb4b16d661d80d41 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -27,7 +27,7 @@ definition Z_of_nat \def
 [ O \Rightarrow  OZ 
 | (S n)\Rightarrow  pos n].
 
-coercion Z_of_nat.
+coercion cic:/matita/Z/z/Z_of_nat.con.
 
 definition neg_Z_of_nat \def
 \lambda n. match n with

diff --git a/helm/matita/library/list/list.ma b/helm/matita/library/list/list.ma
index d5664f4166c783914af3be60f1d60bc25a008a79..ffa2c8ef9ac106c007f701cef1cf21b589f51a19 100644 (file)
--- a/helm/matita/library/list/list.ma
+++ b/helm/matita/library/list/list.ma
@@ -16,6 +16,10 @@ set "baseuri" "cic:/matita/list/".
 include "logic/equality.ma".
 include "higher_order_defs/functions.ma".
 
+inductive list (A:Set) : Set :=
+  | nil: list A
+  | cons: A -> list A -> list A.
+
 notation "hvbox(hd break :: tl)"
   right associative with precedence 46
   for @{'cons $hd $tl}.
@@ -28,10 +32,6 @@ notation "hvbox(l1 break @ l2)"
   right associative with precedence 47
   for @{'append $l1 $l2 }.
 
-inductive list (A:Set) : Set :=
-  | nil: list A
-  | cons: A -> list A -> list A.
-
 interpretation "nil" 'nil = (cic:/matita/list/list.ind#xpointer(1/1/1) _).
 interpretation "cons" 'cons hd tl =
   (cic:/matita/list/list.ind#xpointer(1/1/2) _ hd tl).
@@ -41,8 +41,9 @@ interpretation "cons" 'cons hd tl =
 theorem nil_cons:
   \forall A:Set.\forall l:list A.\forall a:A.
     a::l <> [].
-  intros.
-  unfold; intros.
+  intros;
+  unfold Not;
+  intros;
   discriminate H.
 qed.
 
@@ -64,28 +65,31 @@ definition tail := \lambda A:Set. \lambda l: list A.
 interpretation "append" 'append l1 l2 = (cic:/matita/list/append.con _ l1 l2).
 
 theorem append_nil: \forall A:Set.\forall l:list A.l @ [] = l.
-  intros.
-  elim l.
-  reflexivity.
-  simplify.
-  rewrite > H.
-  reflexivity.
+  intros;
+  elim l;
+  [ reflexivity;
+  | simplify;
+    rewrite > H;
+    reflexivity;
+  ]
 qed.
 
 theorem associative_append: \forall A:Set.associative (list A) (append A).
-  intros; unfold; intros.
-  elim x.
-  simplify; reflexivity.
-  simplify.
-  rewrite > H.
-  reflexivity.
+  intros; unfold; intros;
+  elim x;
+  [ simplify;
+    reflexivity;
+  | simplify;
+    rewrite > H;
+    reflexivity;
+  ]
 qed.
 
 theorem cons_append_commute:
   \forall A:Set.\forall l1,l2:list A.\forall a:A.
     a :: (l1 @ l2) = (a :: l1) @ l2.
-  intros.
-  reflexivity.
+  intros;
+  reflexivity;
 qed.
 
 (*

diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma
index aec51ae8b5f699ea51ff97b06bf17fa2adced7fc..5429b1f82fb0aa427e8d0e55180664b0e2d5c77a 100644 (file)
--- a/helm/matita/tests/coercions.ma
+++ b/helm/matita/tests/coercions.ma
@@ -36,9 +36,9 @@ let rec pos2nat x \def
 
 definition nat2int \def \lambda x. positive x.
 
-coercion pos2nat.
+coercion cic:/matita/tests/coercions/pos2nat.con.
 
-coercion nat2int.
+coercion cic:/matita/tests/coercions/nat2int.con.
 
 definition fst \def \lambda x,y:int.x.
 
@@ -61,4 +61,4 @@ definition double2:
 \def 
   \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)).
   
-  
\ No newline at end of file
+