From cb731a63dfd801c15047e0d18b644794ac63fe03 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 6 Jan 2010 23:03:47 +0000
Subject: [PATCH] Simplified.

Note: it breaks the file later (maybe a coercion conflict, I suppose).
---
 .../matita/nlibrary/overlap/o-algebra.ma      | 35 ++-----------------
 1 file changed, 3 insertions(+), 32 deletions(-)

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
index 89024fe9f..bf320c1e1 100644
--- a/helm/software/matita/nlibrary/overlap/o-algebra.ma
+++ b/helm/software/matita/nlibrary/overlap/o-algebra.ma
@@ -316,51 +316,23 @@ unification hint 0 ≔ P, Q, r;
   
 ninductive one : Type[0] ≝ unit : one.
 
-(*   
-ndefinition force : ∀S:Type[2].∀T1,T2:Type[1].(T1 → T2) → ∀R:S.∀lock:one.Type[2] ≝   
- λS,T1,T2,T,R,lock. match lock with [ unit => S ].
-*)
-
 ndefinition force : ∀S:Type[2]. S → ∀T:Type[2]. T → one → Type[2] ≝   
  λS,s,T,t,lock. match lock with [ unit => S ].
 
-(*
-ndefinition enrich_as : 
- ∀S:Type[2].∀T1,T2:Type[1]. ∀T:T1→T2. ∀R:S.∀lock:one.force S T1 T2 T R lock ≝ 
- λS,T1,T2,T,R,lock. match lock return λlock.match lock with [ unit ⇒ S ] 
-                    with [ unit ⇒ R ].
-*)
-
 ndefinition enrich_as : 
  ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one.force S s T t lock ≝ 
  λS,s,T,t,lock. match lock return λlock.match lock with [ unit ⇒ S ] 
                     with [ unit ⇒ s ].
 
-(*
-ncoercion enrich_as : ∀S:Type[2].∀T1,T2:Type[1].∀T:T1→T2.∀R:S.∀lock:one.force S T1 T2 T R lock
- ≝ enrich_as on T : ? → ? to force ? ? ? ? ? ?.
-*)
-
 ncoercion enrich_as : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock
  ≝ enrich_as on t: ? to force ? ? ? ? ?.
 
-
 (* does not work here 
 nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
 #A; #B; #C; #f; #g; napply(f \circ g).
 nqed.*)
 
-(*
-unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B;
-   lock ≟ unit
-(* --------------------------------------------------------------- *) ⊢
-  (unary_morphism1 A C)
- ≡
-  (force (unary_morphism1 A C) (carr1 A) (carr1 C)
-    (composition1 A B C f g) (comp1_unary_morphisms A B C f g) lock)
-  .
-*)
-
+(* This precise hint does not leave spurious metavariables *)
 unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B;
    lock ≟ unit
 (* --------------------------------------------------------------- *) ⊢
@@ -370,14 +342,13 @@ unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B;
    (carr1 A → carr1 C) (composition1 A B C f g)  lock)
   .
 
-(*
+(* This uniform hint opens spurious metavariables
 unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B, X;
    lock ≟ unit
 (* --------------------------------------------------------------- *) ⊢
   (unary_morphism1 A C)
  ≡
-  (force (unary_morphism1 A C) (carr1 A) (carr1 C)
-    (fun11 … X) (X) lock)
+  (force (unary_morphism1 A C) X (carr1 A → carr1 C) (fun11 … X)  lock)
   .
 *)
 
-- 
2.39.2