X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=a9593c67fb617782815a6631fcc3cfa18c9b5f06;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=53dea97e9c43d2d820f61a96c9f37dff176698b9;hpb=4c1967e287c35d226e773df8d221293c3c74c9d4;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 53dea97e9..a9593c67f 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -506,9 +506,9 @@ and type_of_aux' metasenv context t ugraph =
                      (Some candidate),ugraph4,metasenv,subst
                  | (constructor_args_no,_,instance,_)::tl -> 
                      try
-                       let instance' = 
-                         CicSubstitution.delift constructor_args_no
-                           (CicMetaSubst.apply_subst subst instance)
+                       let instance',subst,metasenv = 
+                         CicMetaSubst.delift_rels subst metasenv
+                          constructor_args_no instance
                        in
                        let candidate,ugraph,metasenv,subst =
                          List.fold_left (
@@ -518,10 +518,9 @@ and type_of_aux' metasenv context t ugraph =
                                | None -> None,ugraph,metasenv,subst
                                | Some ty ->
                                  try 
-                                   let instance' = 
-                                     CicSubstitution.delift
-                                      constructor_args_no
-                                       (CicMetaSubst.apply_subst subst instance)
+                                   let instance',subst,metasenv = 
+                                     CicMetaSubst.delift_rels subst metasenv
+                                      constructor_args_no instance
                                    in
                                    let subst,metasenv,ugraph =
                                     fo_unif_subst subst context metasenv 
@@ -529,7 +528,7 @@ and type_of_aux' metasenv context t ugraph =
                                    in
                                     candidate_oty,ugraph,metasenv,subst
                                  with
-                                    Failure _
+                                    CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
                                   | CicUnification.UnificationFailure _
                                   | CicUnification.Uncertain _ ->
                                      None,ugraph,metasenv,subst
@@ -549,7 +548,7 @@ and type_of_aux' metasenv context t ugraph =
                            Some
                             (add_lambdas 0 t arity_instantiated_with_left_args),
                            ugraph,metasenv,subst
-                     with Failure s -> 
+                     with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                        None,ugraph4,metasenv,subst
                in
                match candidate with