X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=f55b1fed0e646de07d387aacfad9aae8bc60d11f;hb=2fb7dd29bac6ee7add3618c5d798fa60ab0c8eb4;hp=bde5d63e413978703bf8ef0d58a9908f478d1d34;hpb=70211a10f741fe77945f5a720596df2b686f344d;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index bde5d63e4..f55b1fed0 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1104,7 +1104,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
         | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> 
             let t' = CicUniv.fresh() in 
              (try
-              let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
                 C.Sort (C.Type t'),subst,metasenv,ugraph2
               with
@@ -1308,6 +1308,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
                "\n but is applyed to: " ^ String.concat ";" 
                (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
+              let error = ref None in
               let possible_fixes = 
                fix_arity (List.length args) metasenv context subst he hetype
                 ugraph in
@@ -1325,14 +1326,18 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                    with
                     | RefineFailure _ | Uncertain _
                     | HExtlib.Localized (_,RefineFailure _)
-                    | HExtlib.Localized (_,Uncertain _) -> None)
+                    | HExtlib.Localized (_,Uncertain _) as exn ->
+                       error := Some exn; None)
                 possible_fixes
               with
               | Some x -> x
               | None ->
-                 raise 
-                  (MoreArgsThanExpected
-                    (List.length args, RefineFailure (lazy "")))
+                 match !error with
+                    None ->
+                     raise 
+                      (MoreArgsThanExpected
+                        (List.length args, RefineFailure (lazy "")))
+                  | Some exn -> raise exn
     in
     (* first we check if we are in the simple case of a meta closed term *)
     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =