From bc4cc41e813fc850a7f981cd60ba22e14485b7d1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 10 Sep 2009 15:03:13 +0000
Subject: [PATCH] nice hints

---
 helm/software/matita/nlibrary/hints_declaration.ma | 14 +++++++++-----
 helm/software/matita/nlibrary/logic/cprop.ma       |  4 ++--
 helm/software/matita/nlibrary/sets/sets.ma         | 10 +++++-----
 3 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma
index b826d2e76..dac148e4f 100644
--- a/helm/software/matita/nlibrary/hints_declaration.ma
+++ b/helm/software/matita/nlibrary/hints_declaration.ma
@@ -36,7 +36,8 @@ With unidoce and some ASCII art it looks like the following:
 
 *)
    
-notation > "≔ (list0 ( ident x : T ) sep ,) opt (; (list1 (ident U ≟ term 90 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py"
+(* it seems unbelivable, but it works! *)
+notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 90 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py"
   with precedence 90
   for @{ ${ fold right 
                @{ ${ default 
@@ -46,7 +47,11 @@ notation > "≔ (list0 ( ident x : T ) sep ,) opt (; (list1 (ident U ≟ term 90
                     @{ 'hint_decl $Px $Py } 
                  }
                } 
-               rec acc @{ ∀${ident x}:$T.$acc } } }.
+               rec acc @{ 
+                 ${ fold right @{ $acc } rec acc2 
+                      @{ ∀${ident x}:${ default @{ $T } @{ ? } }.$acc2 } } 
+               }
+       }}.
 
 include "logic/pts.ma".
 
@@ -64,12 +69,11 @@ interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a
 interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
 interpretation "hint_decl_Type0"  'hint_decl a b = (hint_declaration_Type0 ? a b).
 
-(* little test 
+(* little test
 naxiom A : Type[0].
 naxiom C : A → A → Type[0].
 ndefinition D ≝ C.               
 alias symbol "hint_decl" = "hint_decl_Type1".
 unification hint 0 ≔ 
-  X : A, Y : A ;  Z ≟ X, W ≟ Y ⊢ C X Y ≡ D Z W.
-  
+  X, R : A, Y ;  Z ≟ X, W ≟ Y ⊢ C X Y ≡ D Z W.
 *)  
diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index 339f73356..e18811da4 100644
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -52,7 +52,7 @@ ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
      | napply (H4 K2)]##]
 nqed.
 
-unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? and_morphism A B) (And A B)).
+unification hint 0 ≔ A,B ⊢ fun21 … and_morphism A B ≡ And A B.
 
 (*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
  #A; #A'; #B; #H1; #H2;
@@ -72,7 +72,7 @@ ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
      | napply (H4 H)]##]
 nqed.
 
-unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? or_morphism A B) (Or A B)).
+unification hint 0 ≔ A,B ⊢ fun21 … or_morphism A B ≡ Or A B.
 
 (*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)
 
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 8553c0fd1..68a281500 100644
--- 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.
-- 
2.39.2