X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2acic.ml;h=f08bb877a1029eac2d5ee939245e76d431a329e0;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=7c18674a865ac9eea2fc2df00b389ebd470ebb3e;hpb=5568099300dd41b552d5be114b2f2c0b97f3c36c;p=helm.git

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 7c18674a8..f08bb877a 100644
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -70,8 +70,8 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
       (*CSC: This is a very inefficient way of computing inner types *)
       (*CSC: and inner sorts: very deep terms have their types/sorts *)
       (*CSC: computed again and again.                               *)
-      let string_of_sort =
-       function 
+      let string_of_sort t =
+       match CicReduction.whd context t with 
           C.Sort C.Prop -> "Prop"
         | C.Sort C.Set  -> "Set"
         | C.Sort C.Type -> "Type"
@@ -100,7 +100,6 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
                match expected with
                   None -> None,false
                 | Some expectedty' ->
-prerr_endline ("###: " ^ CicPp.ppterm synthesized ^ " <==> " ^ CicPp.ppterm expectedty') ; flush stderr ;
                    Some (aux false (Some fresh_id'') context expectedty'),true
             in
              Some
@@ -135,12 +134,20 @@ prerr_endline ("###: " ^ CicPp.ppterm synthesized ^ " <==> " ^ CicPp.ppterm expe
               add_inner_type fresh_id'' ;
              C.AVar (fresh_id'', uri)
           | C.Meta (n,l) ->
+             let (_,canonical_context,_) =
+              List.find (function (m,_,_) -> n = m) metasenv
+             in
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop"  && expected_available then
               add_inner_type fresh_id'' ;
              C.AMeta (fresh_id'', n,
-              (List.map
-                (function None -> None | Some t -> Some (aux' context t)) l))
+              (List.map2
+                (fun ct t ->
+                  match (ct, t) with
+                  | None, _ -> None
+                  | _, Some t -> Some (aux' context t)
+                  | Some _, None -> assert false (* due to typing rules *))
+                canonical_context l))
           | C.Sort s -> C.ASort (fresh_id'', s)
           | C.Implicit -> C.AImplicit (fresh_id'')
           | C.Cast (v,t) ->