ppmetasenv & subst added

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index bde5d63e413978703bf8ef0d58a9908f478d1d34..f55b1fed0e646de07d387aacfad9aae8bc60d11f 100644 (file)
--- 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 =