From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 30 May 2008 09:12:51 +0000 (+0000)
Subject: added a bit more reduction in case Prod v.s. term, was just head_beta_reduce, now... 
X-Git-Tag: make_still_working~5102
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7168611756f3a4c5793cbe978805bb2e93c66cdc;p=helm.git

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

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index ff5f39605..c1e9ea6bc 100644
--- 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