Bug fixed:

 During unification of E1 with E2, E1 and E2 where not always reduced.
 In particular, reduction was not performed in the cases:
   LetIn vs LetIn, Match vs Match
 and maybe also in some cases Appl Meta vs Appl Meta (who knows?)

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d4cb7a53f4c18df105f3a539b72409f6e7d50408..e521dd30144f7db95de3950996dd1c09cd8b54ac 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -572,12 +572,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              (NCicTypeChecker.typeof ~metasenv ~subst context meta)
           in
           let metasenv, subst = 
-           try
-            unify rdb test_eq_only metasenv subst context 
-              (C.Meta (i,l)) lambda_Mj swap
-           with UnificationFailure msg | Uncertain msg when not norm2->
-            (* failure: let's try again argument vs argument *)
-            raise (KeepReducing msg)
+           unify rdb test_eq_only metasenv subst context 
+            (C.Meta (i,l)) lambda_Mj swap
           in
           let metasenv, subst = 
             unify rdb test_eq_only metasenv subst context t1 t2 swap
@@ -612,8 +608,6 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              with
                 Invalid_argument _ -> 
                  raise (Uncertain (mk_msg metasenv subst context t1 t2))
-              | UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
-                 raise (KeepReducing (mk_msg metasenv subst context t1 t2))
               | KeepReducing _ | KeepReducingThis _ -> assert false
            in 
              metasenv, subst
@@ -660,6 +654,12 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
        | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
     in
+    let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
+     try fo_unif test_eq_only metasenv subst nt1 nt2
+     with
+      UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
+       raise (KeepReducing (mk_msg metasenv subst context t1 t2))
+    in
     let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
     (*D*) inside 'H'; try let rc =  
      pp(lazy ("\nProblema:\n" ^