X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=517c013d42b2ac4ffcb6fe7973725561d0fa01da;hb=1bbc2dd649df75e33f2cd7fb3e5ecb15f526a442;hp=ff5f396054795b1fafc2a8567a9da8642143fbf9;hpb=f45e7c2b52e83e4461056d386dcb768d7b25df05;p=helm.git

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index ff5f39605..517c013d4 100644
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -505,12 +505,6 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                               subst context metasenv te t2 ugraph
    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only 
                               subst context metasenv t1 te ugraph
-   | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
-       let subst',metasenv',ugraph1 = 
-         fo_unif_subst true subst context metasenv s1 s2 ugraph 
-       in
-         fo_unif_subst test_equality_only 
-           subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
    | (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 
@@ -767,28 +761,22 @@ res
                 subst context metasenv t1' t2 ugraph         
           | _ -> raise (UnificationFailure (lazy "8")))
 *)
-(* The following idea could be exploited again; right now we have no
-   longer any example requiring it
-   | (C.Prod _, t2) ->
-       let t2' = R.whd ~subst context t2 in
-       (match t2' with
-            C.Prod _ -> 
-              fo_unif_subst test_equality_only 
-                subst context metasenv t1 t2' ugraph         
-          | _ -> raise (UnificationFailure (lazy "8")))
-   | (t1, C.Prod _) ->
-       let t1' = R.whd ~subst context t1 in
-       (match t1' with
-            C.Prod _ -> 
-              fo_unif_subst test_equality_only 
-                subst context metasenv t1' t2 ugraph         
-          | _ -> (* raise (UnificationFailure "9")) *)
-             raise 
-                (UnificationFailure (lazy (sprintf
-                   "Can't unify %s with %s because they are not convertible"
-                   (CicMetaSubst.ppterm ~metasenv subst t1) 
-                   (CicMetaSubst.ppterm ~metasenv subst t2)))))
-*)
+   | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
+       let subst',metasenv',ugraph1 = 
+         fo_unif_subst true subst context metasenv s1 s2 ugraph 
+       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"))))
    | (_,_) ->
      (* delta-beta reduction should almost never be a problem for
         unification since: