X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=09d9ede475cd12bc1a88e34fbf5be307527f1024;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=d64fb005fe79805781ca0a79a10030d492ca2e8a;hpb=d174e54c365ab9df38367de9336c213a03be3c27;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d64fb005f..09d9ede47 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -65,7 +65,7 @@ let eta_reduce subst t =
         | Some bo -> aux (ctx,bo))
     | (name, src)::ctx, (NCic.Appl args as bo) 
       when HExtlib.list_last args = NCic.Rel 1 -> 
-        let args, _ = HExtlib.split_nth (List.length args - 1) args in
+        let args, _ = HExtlib.split_nth "NU 1" (List.length args - 1) args in
         (match delift_if_not_occur (NCic.Appl args) with
         | None -> aux (ctx,NCic.Lambda(name,src, bo)) 
         | Some bo -> aux (ctx,bo))
@@ -302,33 +302,34 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
                   unify hdb test_eq_only metasenv subst context term1 term2
               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
        
-       | NCic.Appl (NCic.Meta (i,l)::args), NCic.Meta (n, _) when 
-         not (NCicMetaSubst.flexible subst args) &&
-         is_locked n subst &&
-         not (List.mem_assoc i subst) 
-         ->
-           (* we verify that none of the args is a Meta, 
-              since beta expanding w.r.t a metavariable makes no sense  *)
-              let metasenv, lambda_Mj =
-                lambda_intros metasenv subst context t1 args
-              in
-              let metasenv, subst = 
-                unify hdb test_eq_only metasenv subst context 
-                  (C.Meta (i,l)) lambda_Mj
-              in
+       | _, NCic.Meta (n, _) when is_locked n subst ->
+           (let (metasenv, subst), i = 
+              match NCicReduction.whd ~subst context t1 with
+              | NCic.Appl (NCic.Meta (i,l)::args) when
+                  not (NCicMetaSubst.flexible subst args) 
+                ->
+                 let metasenv, lambda_Mj =
+                   lambda_intros metasenv subst context t1 args
+                 in
+                   unify hdb test_eq_only metasenv subst context 
+                    (C.Meta (i,l)) lambda_Mj,
+                   i
+              | NCic.Meta (i,_) -> (metasenv, subst), i
+              | _ -> assert false
+             in
               let t1 = NCicReduction.whd ~subst context t1 in
-              let i, l = 
-                match t1 with NCic.Meta (i,l) -> i, l | _ -> assert false
+              let j, lj = 
+                match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
               in
               let metasenv, subst = 
-                instantiate hdb test_eq_only metasenv subst context i l t2 true
+                instantiate hdb test_eq_only metasenv subst context j lj t2 true
               in
               (try
                 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
                 let term = eta_reduce subst term in
                 let subst = List.filter (fun (j,_) -> j <> i) subst in
                 metasenv, ((i, (name, ctx, term, ty)) :: subst)
-              with Not_found -> assert false)
+              with Not_found -> assert false))
 
        | C.Meta (n,lc), t -> 
            (try 
@@ -416,7 +417,10 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
            let relevance = NCicEnvironment.get_relevance r1 in
            let relevance = match r1 with
              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
-                 let _,relevance = HExtlib.split_nth lno relevance in
+                 let relevance =
+                  try snd (HExtlib.split_nth "NU 2" lno relevance)
+                  with Failure _ -> []
+                 in
                    HExtlib.mk_list false lno @ relevance
              | _ -> relevance
            in
@@ -611,8 +615,6 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
  (*D*)  in outside(); rc with exn -> outside (); raise exn 
 ;;
 
-let unify hdb = 
+let unify hdb ?(test_eq_only=false) = 
   indent := "";      
-  unify hdb false;;
-
-
+  unify hdb test_eq_only;;