Added heuristic in the Appl case, we beta-expand only if the argument list

does't contain metas.

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 4cfc796606650dfc22216c0dea6f8baf2fd51059..e521c6570b8958b092bc86a7020b16a3cad0dc20 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -616,61 +616,50 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
                  else
                    beta_reduce (Cic.Appl(he''::tl'))
            | t -> t in
+       let exists_a_meta l = 
+            List.exists (function Cic.Meta _ -> true | _ -> false) l
+       in
         (match l1,l2 with
-(* andrea : this was too powerful. It works very bad with f_equal and
-   similar terms, try and see 
            C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
              (try 
                List.fold_left2 
-                (fun (subst,metasenv) ->
-                   fo_unif_subst test_equality_only subst context metasenv)
-                 (subst,metasenv) l1 l2
+                (fun (subst,metasenv,ugraph) t1 t2 ->
+                   fo_unif_subst 
+                     test_equality_only subst context metasenv t1 t2 ugraph)
+                 (subst,metasenv,ugraph) l1 l2 
              with (Invalid_argument msg) -> raise (UnificationFailure msg)) 
-         | C.Meta (i,l)::args, _ ->
-<<<<<<< cicUnification.ml
-            let subst,metasenv,t2',ugraph1 =
-             beta_expand_many test_equality_only metasenv subst context t2 args
-               ugraph
-            in
-             subst,metasenv,t1,t2',ugraph1
-=======
+         | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
+        (* we verify that none of the args is a Meta, since beta expanding 
+           with respoect to a metavariable makes no sense 
+         *)
             (try 
               let (_,t,_) = CicUtil.lookup_subst i subst in
               let lifted = S.lift_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
               fo_unif_subst 
                 test_equality_only 
-                subst context metasenv reduced t2
+                subst context metasenv reduced t2 ugraph
             with CicUtil.Subst_not_found _ ->
-               let subst,metasenv,beta_expanded =
+               let subst,metasenv,beta_expanded,ugraph1 =
                 beta_expand_many 
-                  test_equality_only metasenv subst context t2 args in
-               fo_unif_subst test_equality_only subst context metasenv 
-                (C.Meta (i,l)) beta_expanded) 
->>>>>>> 1.40
-         | _, C.Meta (i,l)::args ->
-<<<<<<< cicUnification.ml
-            let subst,metasenv,t1',ugraph1 =
-             beta_expand_many test_equality_only metasenv subst context t1 args
-               ugraph
-            in
-             subst,metasenv,t1',t2,ugraph1
-=======
+                  test_equality_only metasenv subst context t2 args ugraph 
+              in
+                 fo_unif_subst test_equality_only subst context metasenv 
+                  (C.Meta (i,l)) beta_expanded ugraph1)
+         | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
             (try 
               let (_,t,_) = CicUtil.lookup_subst i subst in
               let lifted = S.lift_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
               fo_unif_subst 
                 test_equality_only 
-                subst context metasenv t1 reduced
+                subst context metasenv t1 reduced ugraph
             with CicUtil.Subst_not_found _ ->
-               let subst,metasenv,beta_expanded =
+               let subst,metasenv,beta_expanded,ugraph1 =
                 beta_expand_many 
-                  test_equality_only metasenv subst context t1 args in
+                  test_equality_only metasenv subst context t1 args ugraph in
                fo_unif_subst test_equality_only subst context metasenv 
-                (C.Meta (i,l)) beta_expanded)
-*)
-
+                (C.Meta (i,l)) beta_expanded ugraph1)
          | _,_ ->
 (* WAS BEFORE -----
 <<<<<<< cicUnification.ml
@@ -705,7 +694,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
                     test_equality_only subst' metasenv' (l1,l2) ugraph1
              in
                fo_unif_l 
-                test_equality_only subst metasenv (lr1, lr2) ) ugraph(*1*)
+                test_equality_only subst metasenv (lr1, lr2)  ugraph)(**)
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
         fo_unif_subst test_equality_only subst context metasenv outt1 outt2