snapshot

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index b5a4646baba5160bbe940c44d84c38ca8e194b4f..c7d66dd06b4122e6e228410dada0dcf8081e9667 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -382,35 +382,18 @@ let delift metasenv subst context n l t =
                     (metasenv, subst), NCic.Meta(newmeta,l1))
     | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t
   in
-    aux 0 (metasenv,subst) t
-;;
-
-(*
-  in
-   let res =
-    try
-     deliftaux 0 t
-    with
-     NotInTheList ->
+   try aux 0 (metasenv,subst) t
+   with NotInTheList ->
       (* This is the case where we fail even first order unification. *)
       (* The reason is that our delift function is weaker than first  *)
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
-(* debug_print (lazy "First Order UnificationFailure during delift") ;
-debug_print(lazy (sprintf
-        "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
-        (ppterm subst t)
-        (String.concat "; "
-          (List.map
-            (function Some t -> ppterm subst t | None -> "_") l
-          )))); *)
-      let msg = (lazy (sprintf
-        "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
-        (ppterm ~metasenv subst t)
-        (String.concat "; "
-          (List.map
-            (function Some t -> ppterm ~metasenv subst t | None -> "_")
-            l))))
+      let msg = (lazy (Printf.sprintf
+        ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^
+        "abstract over bound variables") (NCicPp.ppterm ~metasenv ~subst
+        ~context t) (String.concat "; " (List.map (NCicPp.ppterm ~metasenv
+        ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift
+        shift) (NCicUtils.expand_local_context lc))))))
       in
        if
          List.exists
@@ -421,11 +404,7 @@ debug_print(lazy (sprintf
         raise (Uncertain msg)
        else
         raise (MetaSubstFailure msg)
-   in
-   let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
-    res, metasenv, subst
 ;;
-*)
 
 (*
 (* delifts a term t of n levels strating from k, that is changes (Rel m)