From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 May 2005 15:26:55 +0000 (+0000)
Subject: When we unify a Prod against a term t2 which is not a Prod we
X-Git-Tag: single_binding~29
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d1d5e134c680aaa1cab15a35b944ca0a3a39c704;p=helm.git

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 130799ea4..1d6044211 100644
--- 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)