prod moved under lambda-prolog unification case

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index c1e9ea6bc834edf1460021b5ce477f1339dca0fd..517c013d42b2ac4ffcb6fe7973725561d0fa01da 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -505,22 +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.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 
@@ -777,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: