added a bit more reduction in case Prod v.s. term, was just head_beta_reduce, now...

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index ff5f396054795b1fafc2a8567a9da8642143fbf9..c1e9ea6bc834edf1460021b5ce477f1339dca0fd 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -511,6 +511,16 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        in
          fo_unif_subst test_equality_only 
            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
+   | (C.Prod _, _) ->
+       (match CicReduction.whd ~subst context t2 with
+        | C.Prod _ as t2 -> 
+            fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+        | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
+   | (_, C.Prod _) ->
+       (match CicReduction.whd ~subst context t1 with
+        | C.Prod _ as t1 -> 
+            fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+        | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
        let subst',metasenv',ugraph1 = 
          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph