Names of some constructors changed.

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

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index b9a79b64ff74b0ec71eb80e54e8024a224a6984c..024f49ebf6732ca6bf4ad6e82d5011007c1012b7 100644 (file)
--- a/helm/gTopLevel/doubleTypeInference.ml
+++ b/helm/gTopLevel/doubleTypeInference.ml
@@ -463,8 +463,6 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           (* the synthesized type. Let's forget it.       *)
           {synthesized = synthesized' ; expected = None}, synthesized
        | Some expectedty' ->
-prerr_endline ("t: " ^ CicPp.ppterm t) ; flush stderr ;
-prerr_endline (CicPp.ppterm synthesized' ^ " <-> " ^ CicPp.ppterm expectedty') ; flush stderr ;
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index 2812bd64e02f352c824c17d0bb3eb8260f594bbe..093f0228cfc7b7696010b6610b4305808838f435 100644 (file)
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -72,8 +72,8 @@ let out_func = function
 
 let out_str = function
    | MQCons s      -> con s
-   | MQRVar s      -> out_rvar s
-   | MQSVar s      -> out_svar s
+   | MQSRVar s      -> out_rvar s
+   | MQSSVar s      -> out_svar s
    | MQFunc (f, r) -> out_func f ^ out_rvar r
    | MQMConclusion -> key "mainconclusion" 
    | MQConclusion  -> key "conclusion" 
@@ -98,7 +98,7 @@ and out_list = function
    | MQPattern p -> key "pattern" ^ out_pat p
    | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
    | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
-   | MQRVarOccur v -> key "rvaroccur" ^ v
+   | MQLRVar v -> key "rvaroccur" ^ v
 
 let out_query = function
    | MQList l -> out_list l
@@ -244,7 +244,7 @@ let build_select (r, b, v) n =
    let mqs = if b then MQMConclusion else MQConclusion in
    MQSelect (rvar, 
              MQUse (MQPattern r, svar),
-             MQIs (MQSVar svar, mqs)
+             MQIs (MQSSVar svar, mqs)
             )
 
 let rec build_inter n = function
@@ -274,10 +274,10 @@ let restrict_universe query =
         MQSubset (
          MQSelect (
           "uri2",
-          MQUsedBy (MQRVarOccur "uri", "pos"),
+          MQUsedBy (MQLRVar "uri", "pos"),
           MQOr (
-           MQIs (MQSVar "pos", MQConclusion),
-           MQIs (MQSVar "pos", MQMConclusion)
+           MQIs (MQSSVar "pos", MQConclusion),
+           MQIs (MQSSVar "pos", MQMConclusion)
           )
          ),
          universe