From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 19 Nov 2005 09:00:58 +0000 (+0000)
Subject: Coercions are now inserted also around the sources of lambda abstractions.
X-Git-Tag: V_0_7_2_3~32
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=d3eb189f3d8dc8371e5c4c4735ba27c72fef1d74;p=helm.git

Coercions are now inserted also around the sources of lambda abstractions.
---

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
index 579708e6f..010595e09 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
@@ -24,4 +24,5 @@ include "qd_defs.ma".
 definition Subset \def \forall (D:QD). D \to Prop.
 
 alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
-definition stop \def \lambda (D:QD). \lambda (a:(ac (qd D))). True.
+
+definition stop \def \lambda (D:QD). \lambda (a:D). True.
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 37d89bf1f..681ed4929 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -426,22 +426,28 @@ and type_of_aux' metasenv context t ugraph =
         | C.Lambda (n,s,t) ->
 
             let s',sort1,subst',metasenv',ugraph1 = 
-              type_of_aux subst metasenv context s ugraph
-            in
-            (match CicReduction.whd ~subst:subst' context sort1 with
+              type_of_aux subst metasenv context s ugraph in
+            let s',sort1 =
+             match CicReduction.whd ~subst:subst' context sort1 with
                  C.Meta _
-               | C.Sort _ -> ()
-               | _ ->
-                   raise (RefineFailure (lazy (sprintf
-                                           "Not well-typed lambda-abstraction: the source %s should be a type;
-           instead it is a term of type %s" (CicPp.ppterm s)
-                                           (CicPp.ppterm sort1))))
-            ) ;
+               | C.Sort _ -> s',sort1
+               | coercion_src ->
+                  let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in
+                  let search = CoercGraph.look_for_coercion in
+                  let boh = search coercion_src coercion_tgt in
+                   match boh with
+                    | CoercGraph.SomeCoercion c -> 
+                       Cic.Appl [c;s'], coercion_tgt
+                  | CoercGraph.NoCoercion
+                  | CoercGraph.NotHandled _
+                  | CoercGraph.NotMetaClosed -> 
+                     raise (RefineFailure (lazy (sprintf
+                      "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))))
+            in
             let context_for_t = ((Some (n,(C.Decl s')))::context) in 
             let metasenv',t = exp_impl metasenv' subst' context_for_t t in
             let t',type2,subst'',metasenv'',ugraph2 =
-              type_of_aux subst' metasenv' 
-                context_for_t t ugraph1
+              type_of_aux subst' metasenv' context_for_t t ugraph1
             in
               C.Lambda (n,s',t'),C.Prod (n,s',type2),
                 subst'',metasenv'',ugraph2