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 579708e6f55e7601ee6732eb3559f4ec48f6218c..010595e09176087d81ead195237b811f415864f5 100644 (file)
--- 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 37d89bf1f300c279d39e36eea0dd9f15c2d7b83d..681ed492979851c963abbbf27ad9b3f181008a10 100644 (file)
--- 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