X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=271f9a0404b10d9d217997f57bda007058e15f46;hb=e356b6fba9e8fd1e757e7589f01fb9b51979f76c;hp=9a6358baaf3e98ee5d4de13bd12e3ee9c02e2e61;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index 9a6358baa..271f9a040 100644
--- a/matita/components/ng_tactics/nTacStatus.ml
+++ b/matita/components/ng_tactics/nTacStatus.ml
@@ -29,9 +29,12 @@ let wrap fname f x =
   with 
   | MultiPassDisambiguator.DisambiguationError _ 
   | NCicRefiner.RefineFailure _ 
+  | NCicRefiner.Uncertain _ 
   | NCicUnification.UnificationFailure _ 
+  | NCicUnification.Uncertain _ 
   | NCicTypeChecker.TypeCheckerFailure _ 
-  | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
+  | NCicMetaSubst.MetaSubstFailure _
+  | NCicMetaSubst.Uncertain _ as exn -> fail ~exn (lazy fname)
 ;;
 
 class type g_eq_status =
@@ -157,7 +160,7 @@ let relocate status destination (source,t as orig) =
             let u, d, metasenv, subst, o = status#obj in
             pp(lazy("delifting as " ^ 
               status#ppterm ~metasenv ~subst ~context:source 
-               (NCic.Meta (0,lc))));
+               (NCic.Meta (-1,lc))));
             let (metasenv, subst), t =
               NCicMetaSubst.delift status
                  ~unify:(fun m s c t1 t2 -> 
@@ -165,7 +168,7 @@ let relocate status destination (source,t as orig) =
                    with 
                     | NCicUnification.UnificationFailure _ 
                     | NCicUnification.Uncertain _ -> None) 
-               metasenv subst source 0 lc t
+               metasenv subst source (-1) lc t
             in
             let status = status#set_obj (u, d, metasenv, subst, o) in
             status, (ctx,t))
@@ -397,7 +400,7 @@ let select_term
         let ctx = (n, NCic.Decl s2) :: ctx in
         let status, t = select status ctx t1 t2 in
         status, NCic.Prod (n,s,t)
-    | NCic.Appl l1, NCic.Appl l2 ->
+    | NCic.Appl l1, NCic.Appl l2 when List.length l1 = List.length l2 ->
         let status, l = 
            List.fold_left2
              (fun (status,l) x y -> 
@@ -406,7 +409,8 @@ let select_term
              (status,[]) l1 l2
         in
         status, NCic.Appl (List.rev l)
-    | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) ->
+    | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2)
+      when List.length pl1 = List.length pl2 ->
         let status, t = select status ctx t1 t2 in
         let status, ot = select status ctx ot1 ot2 in
         let status, pl =