nice hints

[helm.git] / helm / software / matita / nlibrary / sets / sets.ma

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 8553c0fd1810b98b39d28a7156eb8472a3d6b1b0..68a281500480d917106be8d0495182123dcfff29 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -71,7 +71,7 @@ nqed.
 include "hints_declaration.ma". 
 
 alias symbol "hint_decl" = "hint_decl_Type2".
-unification hint 0 ≔ A : ? ⊢ carr1 (powerclass_setoid A) ≡ Ω^A.
+unification hint 0 ≔ A ⊢ carr1 (powerclass_setoid A) ≡ Ω^A.
 
 (************ SETS OVER SETOIDS ********************)
 
@@ -104,7 +104,7 @@ ndefinition qpowerclass_setoid: setoid → setoid1.
   | napply (qseteq A) ]
 nqed.
 
-unification hint 0 ≔ A : ? ⊢  
+unification hint 0 ≔ A ⊢  
   carr1 (qpowerclass_setoid A) ≡ qpowerclass A.
 
 nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP.
@@ -118,7 +118,7 @@ nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid
 nqed.
 
 unification hint 0 ≔ 
-  A : setoid, x : ?, S : ? ⊢ (mem_ok A) x S ≡ mem A S x.
+  A : setoid, x, S ⊢ (mem_ok A) x S ≡ mem A S x.
   
 nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
  #A; napply mk_binary_morphism1
@@ -145,11 +145,11 @@ nqed.
 (* unfold if intersect, exposing fun21 *)
 alias symbol "hint_decl" = "hint_decl_Type1".
 unification hint 0 ≔ 
-  A : setoid, B : qpowerclass A, C : qpowerclass A ⊢ 
+  A : setoid, B,C : qpowerclass A ⊢ 
     pc A (intersect_ok A B C) ≡ intersect ? (pc ? B) (pc ? C).
 
 (* hints can pass under mem *) (* ??? XXX why is it needed? *)
-unification hint 0 ≔ A:?, B:?, x:?;
+unification hint 0 ≔ A,B,x ;
            C ≟ B
  (*---------------------*) ⊢ 
    mem A B x ≡ mem A C x.