Names of some constructors changed.

[helm.git] / helm / gTopLevel / cic2acic.ml

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 81e94419699624d13c167accbe0b8bccff80f3e7..df3bdabf905f56cde36802c5f7fe9c8a82ae41f5 100644 (file)
--- 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