Beta-expansion was avoided as soon as one argument was flexible.

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index be7a2fe4cab899551151f4745d5fed2851d57cd1..795b8504296249d2e624d8005a776c2cd2eaa4cb 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -343,9 +343,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
        | _, 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) 
-                ->
+              | NCic.Appl (NCic.Meta (i,l)::args) ->
                  let metasenv, subst, lambda_Mj =
                    lambda_intros rdb metasenv subst context t1 args
                  in
@@ -423,45 +421,41 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
             with Invalid_argument _ -> 
               raise (fail_exc metasenv subst context t1 t2))
 
-       | NCic.Appl (NCic.Meta (i,l)::args), _ when 
-         not (NCicMetaSubst.flexible subst args) ->
-           (* we verify that none of the args is a Meta, 
-              since beta expanding w.r.t a metavariable makes no sense  *)
-              let metasenv, subst, lambda_Mj =
-                lambda_intros rdb metasenv subst context t1 args
-              in
-              let metasenv, subst = 
-                unify rdb test_eq_only metasenv subst context 
-                  (C.Meta (i,l)) lambda_Mj
-              in
-              let metasenv, subst = 
-                unify rdb test_eq_only metasenv subst context t1 t2 
-              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)
-
-       | _, NCic.Appl (NCic.Meta (i,l)::args) when 
-         not(NCicMetaSubst.flexible subst args) ->
-              let metasenv, subst, lambda_Mj =
-                lambda_intros rdb metasenv subst context t2 args
-              in
-              let metasenv, subst =
-                unify rdb test_eq_only metasenv subst context 
-                 lambda_Mj (C.Meta (i,l))
-              in
-              let metasenv, subst = 
-                unify rdb test_eq_only metasenv subst context t1 t2 
-              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)
+       | NCic.Appl (NCic.Meta (i,l)::args), _ ->
+          let metasenv, subst, lambda_Mj =
+            lambda_intros rdb metasenv subst context t1 args
+          in
+          let metasenv, subst = 
+            unify rdb test_eq_only metasenv subst context 
+              (C.Meta (i,l)) lambda_Mj
+          in
+          let metasenv, subst = 
+            unify rdb test_eq_only metasenv subst context t1 t2 
+          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)
+
+       | _, NCic.Appl (NCic.Meta (i,l)::args) ->
+         let metasenv, subst, lambda_Mj =
+           lambda_intros rdb metasenv subst context t2 args
+         in
+         let metasenv, subst =
+           unify rdb test_eq_only metasenv subst context 
+            lambda_Mj (C.Meta (i,l))
+         in
+         let metasenv, subst = 
+           unify rdb test_eq_only metasenv subst context t1 t2 
+         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)
 
        (* processing this case here we avoid a useless small delta step *)
        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))