When we unify a Prod against a term t2 which is not a Prod we

now try a whd of t2.

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 130799ea432a7ee1426d7645099c0c40e6a4c5d4..1d6044211ebd60737bd8137a4299a8520b45c3b8 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -46,18 +46,6 @@ let type_of_aux' metasenv subst context term ugraph =
              (CicMetaSubst.ppmetasenv metasenv subst) 
              (CicMetaSubst.ppsubst subst) msg) in
         raise (AssertFailure msg);;
-(*
->>>>>>> 1.40
-  try
-    CicMetaSubst.type_of_aux' metasenv subst context term ugraph
-  with
-  | CicMetaSubst.MetaSubstFailure msg ->
-    raise (AssertFailure
-      ((sprintf
-        "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
-        (CicMetaSubst.ppterm subst term)
-        (CicMetaSubst.ppcontext subst context)
-        (CicMetaSubst.ppmetasenv metasenv subst) msg))) *)
 
 let rec deref subst =
   let snd (_,a,_) = a in
@@ -661,16 +649,6 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
                fo_unif_subst test_equality_only subst context metasenv 
                 (C.Meta (i,l)) beta_expanded ugraph1)
          | _,_ ->
-(* WAS BEFORE -----
-<<<<<<< cicUnification.ml
-             subst,metasenv,t1,t2,ugraph
-       in
-        begin
-         match t1',t2' with
-            C.Appl l1, C.Appl l2 ->
-             let lr1 = List.rev l1 in
-=======
---------*)
             let lr1 = List.rev l1 in
              let lr2 = List.rev l2 in
              let rec 
@@ -741,6 +719,20 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
                  "Can't unify %s with %s because they are not convertible"
                  (CicMetaSubst.ppterm subst t1) 
                  (CicMetaSubst.ppterm subst t2))) *)
+   | (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 "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"))
    | (_,_) ->
        let b,ugraph1 = 
         R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
@@ -748,7 +740,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
         if b then 
            subst, metasenv, ugraph1
         else
-           raise (UnificationFailure "8")
+           raise (UnificationFailure "10")
              (* (sprintf
                "Can't unify %s with %s because they are not convertible"
                (CicMetaSubst.ppterm subst t1)