Refinement bug fixed. The outtype was not refined if it was an Implicit.

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index f050726bcc70034f6844e1ebc110ab3fc71c424c..239db16cf11560a552531c03ee2aebe83fa2be1d 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -528,6 +528,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 its instances 
              *)
              
+           let outtype,outtypety, subst, metasenv,ugraph4 =
+             type_of_aux subst metasenv context outtype ugraph4 in
            (match outtype with
            | C.Meta (n,l) ->
                (let candidate,ugraph5,metasenv,subst = 
@@ -660,9 +662,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                         (Cic.Appl (outtype::right_args@[term']))),
                      subst,metasenv,ugraph)
            | _ ->    (* easy case *)
-             let outtype,outtypety, subst, metasenv,ugraph4 =
-               type_of_aux subst metasenv context outtype ugraph4
-             in
              let tlbody_and_type,subst,metasenv,ugraph4 =
                List.fold_right
                  (fun x (res,subst,metasenv,ugraph) ->