CicSubstitution.delift ==> CicMetaSubst.delift_rels

[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 57e4c5e9d6fff45e438c96cc7f4b3f781ee71700..e64499b3b94a819723a603fe803efab7fc067a91 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -507,7 +507,7 @@ and type_of_aux' metasenv context t ugraph =
                  | (constructor_args_no,_,instance,_)::tl -> 
                      try
                        let instance' = 
-                         CicSubstitution.delift constructor_args_no
+                         CicMetaSubst.delift_rels constructor_args_no
                            (CicMetaSubst.apply_subst subst instance)
                        in
                        let candidate,ugraph,metasenv,subst =
@@ -519,7 +519,7 @@ and type_of_aux' metasenv context t ugraph =
                                | Some ty ->
                                  try 
                                    let instance' = 
-                                     CicSubstitution.delift
+                                     CicMetaSubst.delift_rels
                                       constructor_args_no
                                        (CicMetaSubst.apply_subst subst instance)
                                    in
@@ -529,7 +529,7 @@ and type_of_aux' metasenv context t ugraph =
                                    in
                                     candidate_oty,ugraph,metasenv,subst
                                  with
-                                    CicSubstitution.DeliftingWouldCaptureAFreeVariable
+                                    CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
                                   | CicUnification.UnificationFailure _
                                   | CicUnification.Uncertain _ ->
                                      None,ugraph,metasenv,subst
@@ -549,7 +549,7 @@ and type_of_aux' metasenv context t ugraph =
                            Some
                             (add_lambdas 0 t arity_instantiated_with_left_args),
                            ugraph,metasenv,subst
-                     with CicSubstitution.DeliftingWouldCaptureAFreeVariable -> 
+                     with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                        None,ugraph4,metasenv,subst
                in
                match candidate with