X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2acic.ml;h=df3bdabf905f56cde36802c5f7fe9c8a82ae41f5;hb=528294d5228f65f4b3fbd3ebe00a5cd9a8f3b929;hp=81e94419699624d13c167accbe0b8bccff80f3e7;hpb=d7e5adc6adcdcbc98964fa73b3d8e05cad428a6b;p=helm.git

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 81e944196..df3bdabf9 100644
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -77,7 +77,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
         | C.Sort C.Type -> "Type"
         | _ -> assert false
       in
-       let ainnertypes,innertype,innersort =
+       let ainnertypes,innertype,innersort,expected_available =
 (*CSC: Here we need the algorithm for Coscoy's double type-inference  *)
 (*CSC: (expected type + inferred type). Just for now we use the usual *)
 (*CSC: type-inference, but the result is very poor. As a very weak    *)
@@ -94,21 +94,23 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
            D.expected = None}
         in
          let innersort = T.type_of_aux' metasenv context synthesized in
-          let ainnertypes =
+          let ainnertypes,expected_available =
            if computeinnertypes then
-            Some
-             {annsynthesized =
-               aux false (Some fresh_id'') context synthesized ;
-              annexpected =
+            let annexpected,expected_available =
                match expected with
-                  None -> None
+                  None -> None,false
                 | Some expectedty' ->
-                   Some (aux false (Some fresh_id'') context expectedty')
-             }
+                   Some (aux false (Some fresh_id'') context expectedty'),true
+            in
+             Some
+              {annsynthesized =
+                aux false (Some fresh_id'') context synthesized ;
+               annexpected = annexpected
+              }, expected_available
            else
-            None
+            None,false
           in
-           ainnertypes, synthesized, string_of_sort innersort
+           ainnertypes,synthesized, string_of_sort innersort, expected_available
        in
         let add_inner_type id =
          match ainnertypes with
@@ -157,7 +159,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
                        C.Lambda _ -> true
                      | _ -> false
                in
-                if not father_is_lambda then
+                if (not father_is_lambda) || expected_available then
                  add_inner_type fresh_id''
               end ;
              C.ALambda