From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 27 May 2005 11:01:16 +0000 (+0000)
Subject: 1. removed obsolete comments
X-Git-Tag: PRE_INDEX_1~116
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2468d0398195d41200bfd07db68fa675dc90b875;p=helm.git

1. removed obsolete comments
2. extended delift to the case of meta in head position
3. added a cases (? t1) vs t2: ? gets unified to the beta
expansion of t2 w.r.t t1.
---

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 1d6044211..25db7d915 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -47,6 +47,19 @@ let type_of_aux' metasenv subst context term ugraph =
              (CicMetaSubst.ppsubst subst) msg) in
         raise (AssertFailure msg);;
 
+let exists_a_meta l = 
+  List.exists (function Cic.Meta _ -> true | _ -> false) l
+
+let rec beta_reduce =
+  function
+      (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+        let he'' = CicSubstitution.subst he' t in
+          if tl' = [] then
+            he''
+          else
+            beta_reduce (Cic.Appl(he''::tl'))
+    | t -> t
+(* 
 let rec deref subst =
   let snd (_,a,_) = a in
   function
@@ -58,7 +71,26 @@ let rec deref subst =
 	 with 
 	   CicUtil.Subst_not_found _ -> t)
     | t -> t
-;;
+;; *)
+
+let rec deref subst t =
+  let snd (_,a,_) = a in
+  match t with
+      Cic.Meta(n,l) -> 
+	(try 
+	   deref subst
+	     (CicSubstitution.subst_meta 
+		l (snd (CicUtil.lookup_subst n subst))) 
+	 with 
+	     CicUtil.Subst_not_found _ -> t)
+    | Cic.Appl(Cic.Meta(n,l)::args) ->
+	(match deref subst (Cic.Meta(n,l)) with
+	   | Cic.Lambda _ as t -> 
+	       deref subst (beta_reduce (Cic.Appl(t::args)))
+	   | r -> Cic.Appl(r::args))
+    | t -> t
+;; 
+
 
 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
  let module S = CicSubstitution in
@@ -82,21 +114,6 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
            let subst,metasenv,exp_named_subst',ugraph1 =
             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
            in
-(* THIS WAS BEFORE ----
-            subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
-        | C.Meta (i,l) as t->
-           (try
-             let (_, t') = CicMetaSubst.lookup_subst i subst in
-             aux metasenv subst n context (CicSubstitution.subst_meta l t')
-               ugraph
-            with CicMetaSubst.SubstNotFound _ ->
-              let (subst, metasenv, context, local_context,ugraph1) =
-                List.fold_left
-                  (fun (subst, metasenv, context, local_context,ugraph) t ->
-                    match t with
-                    | None -> 
-                        (subst, metasenv, context, None::local_context, ugraph)
---------- *)
             subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
         | C.Meta (i,l) ->
 	    (* andrea: in general, beta_expand can create badly typed
@@ -109,29 +126,6 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
 		     Some t -> Some (CicSubstitution.lift 1 t)
 		   | None -> None) l in
 	    subst, metasenv, C.Meta (i,l), ugraph
-            (*
-            let (subst, metasenv, context, local_context) =
-              List.fold_right
-                (fun t (subst, metasenv, context, local_context) ->
-                   match t with
-                    | None -> (subst, metasenv, context, None :: local_context)
-
-                    | Some t ->
-                        let (subst, metasenv, t, ugraph1) =
-                          aux metasenv subst n context t ugraph
-                        in
-(* THIS WAS BEFORE ----
-                        (subst, metasenv, context,
-                        (Some t)::local_context,ugraph1))
-                  (subst, metasenv, context, [],ugraph) l
-              in
-              (subst, metasenv,(C.Meta (i, local_context)),ugraph1))
--------- *)
-                          (subst, metasenv, context, Some t :: local_context))
-                l (subst, metasenv, context, [])
-            in
-  prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context))));
-              (subst, metasenv, C.Meta (i, local_context)) *)
         | C.Sort _
         | C.Implicit _ as t -> subst,metasenv,t,ugraph
         | C.Cast (te,ty) ->
@@ -217,7 +211,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
             in
              C.Fix (i, substitutedfl)
 *)
-   subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
+	    subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
         | C.CoFix (i,fl) ->
 (*CSC: not implemented
            let tylen = List.length fl in
@@ -229,7 +223,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
              C.CoFix (i, substitutedfl)
 
 *) 
-    subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
+	    subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
 
   and aux_exp_named_subst metasenv subst n context ens ugraph =
    List.fold_right
@@ -243,20 +237,9 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
     metasenv context (Cic.Name "Heta") ~typ:argty
   in
    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
- (* prova *)
- (* old 
-    subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
- *)
-    subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2
+   subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2
 
 
-(* WAS ---------
-and beta_expand_many test_equality_only metasenv subst context t l ugraph =
- List.fold_left
-  (fun (subst,metasenv,t,ugraph) arg ->
-    beta_expand test_equality_only metasenv subst context t arg ugraph
-  ) (subst,metasenv,t,ugraph) l
-------- *)
 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
   let subst,metasenv,hd,ugraph =
     List.fold_right
@@ -292,63 +275,23 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
    if b then
      subst, metasenv, ugraph 
    else
-     match (t1, t2) with
-	 (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
-(*
-       let ok,subst,metasenv,ugraph1 =
-       try
-        List.fold_left2
-         (fun (b,subst,metasenv,ugraph) t1 t2 ->
-           if b then true,subst,metasenv,ugraph else
-            match t1,t2 with
-               None,_
-             | _,None -> true,subst,metasenv,ugraph
-             | Some t1', Some t2' ->
-                (* First possibility:  restriction    *)
-                (* Second possibility: unification    *)
-                (* Third possibility:  convertibility *)
-                let b',ugraph1 = 
-                  R.are_convertible subst context t1' t2' ugraph in
-                if b' then
-                  true,subst,metasenv,ugraph1
-                else
-                 (try
-                   let subst,metasenv,ugraph2 =
-                    fo_unif_subst 
-                     (* TASSI: is this another try that should use ugraph? *)
-                     test_equality_only subst context metasenv t1' t2' ugraph
-                   in
-                    true,subst,metasenv,ugraph2
-                 with
-                  Not_found -> false,subst,metasenv,ugraph1)
-         ) (true,subst,metasenv,ugraph) ln lm
-       with
-        Invalid_argument _ ->
-         raise (UnificationFailure (sprintf
-           "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
-       in
-        if ok then
-          subst,metasenv,ugraph1
-        else
-          raise (UnificationFailure (sprintf
-            "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
-            (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
-	  *)
-       let _,subst,metasenv,ugraph1 =
-	 (try
-            List.fold_left2
-              (fun (j,subst,metasenv,ugraph) t1 t2 ->
-		 match t1,t2 with
-		     None,_
-		   | _,None -> j+1,subst,metasenv,ugraph
-		   | Some t1', Some t2' ->
-                       (* First possibility:  restriction    *)
-                       (* Second possibility: unification    *)
-                       (* Third possibility:  convertibility *)
-		       let b, ugraph1 = 
+   match (t1, t2) with
+     | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
+	 let _,subst,metasenv,ugraph1 =
+	   (try
+              List.fold_left2
+		(fun (j,subst,metasenv,ugraph) t1 t2 ->
+		   match t1,t2 with
+		       None,_
+		     | _,None -> j+1,subst,metasenv,ugraph
+		     | Some t1', Some t2' ->
+			 (* First possibility:  restriction    *)
+			 (* Second possibility: unification    *)
+			 (* Third possibility:  convertibility *)
+			 let b, ugraph1 = 
 			 R.are_convertible 
 			   ~subst ~metasenv context t1' t2' ugraph
-		       in
+			 in
 			 if b then
 			   j+1,subst,metasenv, ugraph1 
 			 else
@@ -363,117 +306,46 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
 				Uncertain _
 			      | UnificationFailure _ ->
 prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)); 
-				let metasenv, subst = 
-				  CicMetaSubst.restrict 
-				    subst [(n,j)] metasenv in
-				  j+1,subst,metasenv,ugraph1)
-	      ) (1,subst,metasenv,ugraph) ln lm
-	  with
-	      Exit ->
-		raise 
-		(UnificationFailure "1")
-(*
-		   (sprintf
+				  let metasenv, subst = 
+				    CicMetaSubst.restrict 
+				      subst [(n,j)] metasenv in
+				    j+1,subst,metasenv,ugraph1)
+		) (1,subst,metasenv,ugraph) ln lm
+	    with
+		Exit ->
+		  raise 
+		    (UnificationFailure "1")
+		    (*
+		    (sprintf
 		      "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
-		      (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
-	    | Invalid_argument _ ->
-		raise 
-		  (UnificationFailure "2"))
-(*
-		     (sprintf
-			"Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))*)
-       in subst,metasenv,ugraph1
-
-   | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
-       fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
-   | (C.Meta (n,l), t)   
-   | (t, C.Meta (n,l)) ->
-       let swap =
-        match t1,t2 with
-           C.Meta (n,_), C.Meta (m,_) when n < m -> false
-         | _, C.Meta _ -> false
-         | _,_ -> true
-       in
-       let lower = fun x y -> if swap then y else x in
-       let upper = fun x y -> if swap then x else y in
-       let fo_unif_subst_ordered 
-        test_equality_only subst context metasenv m1 m2 ugraph =
-          fo_unif_subst test_equality_only subst context metasenv 
-           (lower m1 m2) (upper m1 m2) ugraph
-       in
-(*
-        begin
-        try
-          let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-          let lifted_oldt = S.subst_meta l oldt in
-          let ty_lifted_oldt,ugraph1 =
-            type_of_aux' metasenv subst context lifted_oldt ugraph
-          in
-          let tyt,ugraph2 = type_of_aux' metasenv subst context t ugraph1 in
-          let (subst, metasenv, ugraph3) =
-            fo_unif_subst_ordered test_equality_only subst context metasenv
-              tyt ty_lifted_oldt ugraph2
-          in
-          fo_unif_subst_ordered 
-            test_equality_only subst context metasenv t lifted_oldt ugraph3
-        with CicMetaSubst.SubstNotFound _ ->
-         (* First of all we unify the type of the meta with the type of the term *)
-         let subst,metasenv,ugraph1 =
-          let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
-          (try
-            let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in
-             fo_unif_subst 
-              test_equality_only 
-               subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
-          with AssertFailure _ ->
-            (* TODO huge hack!!!!
-             * we keep on unifying/refining in the hope that the problem will be
-             * eventually solved. In the meantime we're breaking a big invariant:
-             * the terms that we are unifying are no longer well typed in the
-             * current context (in the worst case we could even diverge)
-             *)
-(*
-prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
-prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
-*)
-            (subst, metasenv,ugraph))
-         in
-          let t',metasenv,subst =
-           try
-             (* TASSI:  I hope delift does nothing with universes *)
-             CicMetaSubst.delift n subst context metasenv l t
-           with
-              (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
-            | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
-          in
-           let t'',ugraph2 =
-            match t' with
-               C.Sort (C.Type u) when not test_equality_only ->
-                 let u' = CicUniv.fresh () in
-                 let s = C.Sort (C.Type u') in
-                 let ugraph2 =
-                   CicUniv.add_ge (upper u u') (lower u u') ugraph1 in
-                 s,ugraph2
-              | _ -> t',ugraph1
-           in
-            (* Unifying the types may have already instantiated n. Let's check *)
-            try
-             let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-             let lifted_oldt = S.subst_meta l oldt in
-              fo_unif_subst_ordered 
-               test_equality_only subst context metasenv t lifted_oldt ugraph2
-            with
-             CicMetaSubst.SubstNotFound _ -> 
-               let (_, context, _) = CicUtil.lookup_meta n metasenv in
-               let subst = (n, (context, t'')) :: subst in
-               let metasenv =
-(*                 CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
-                CicMetaSubst.apply_subst_metasenv subst metasenv
-               in
-               subst, metasenv,ugraph2
-(*               (n,t'')::subst, metasenv *)
-        end
-*)
+		      (CicMetaSubst.ppterm subst t1) 
+		      (CicMetaSubst.ppterm subst t2))) *)
+	      | Invalid_argument _ ->
+		  raise 
+		    (UnificationFailure "2"))
+	            (*
+		    (sprintf
+		      "Error trying to unify %s with %s: the lengths of the two local contexts do not match." 
+		      (CicMetaSubst.ppterm subst t1) 
+		      (CicMetaSubst.ppterm subst t2)))) *)
+	 in subst,metasenv,ugraph1
+     | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
+	 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
+     | (C.Meta (n,l), t)   
+     | (t, C.Meta (n,l)) ->
+	 let swap =
+           match t1,t2 with
+               C.Meta (n,_), C.Meta (m,_) when n < m -> false
+             | _, C.Meta _ -> false
+             | _,_ -> true
+	 in
+	 let lower = fun x y -> if swap then y else x in
+	 let upper = fun x y -> if swap then x else y in
+	 let fo_unif_subst_ordered 
+             test_equality_only subst context metasenv m1 m2 ugraph =
+           fo_unif_subst test_equality_only subst context metasenv 
+             (lower m1 m2) (upper m1 m2) ugraph
+	 in
          begin
          let subst,metasenv,ugraph1 =
            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
@@ -530,8 +402,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 	       let metasenv =
 		 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
 	       subst, metasenv, ugraph2
-         end
-
+	 end
    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
       if UriManager.eq uri1 uri2 then
@@ -539,28 +410,33 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
         exp_named_subst1 exp_named_subst2 ugraph
       else
        raise (UnificationFailure "3")
-       (* (sprintf
-        "Can't unify %s with %s due to different constants"
-        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
+	 (* (sprintf
+            "Can't unify %s with %s due to different constants"
+            (CicMetaSubst.ppterm subst t1) 
+	    (CicMetaSubst.ppterm subst t2))) *)
    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
-      if UriManager.eq uri1 uri2 && i1 = i2 then
-       fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
-        exp_named_subst1 exp_named_subst2 ugraph
-      else
-       raise (UnificationFailure "4")
-        (* (sprintf
-        "Can't unify %s with %s due to different inductive principles"
-        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
+       if UriManager.eq uri1 uri2 && i1 = i2 then
+	 fo_unif_subst_exp_named_subst 
+	   test_equality_only 
+	   subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
+       else
+	 raise (UnificationFailure "4")
+           (* (sprintf
+              "Can't unify %s with %s due to different inductive principles"
+              (CicMetaSubst.ppterm subst t1) 
+	      (CicMetaSubst.ppterm subst t2))) *)
    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
-     C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
-      if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
-       fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
-        exp_named_subst1 exp_named_subst2 ugraph
-      else
-       raise (UnificationFailure "5")
-       (* (sprintf
-        "Can't unify %s with %s due to different inductive constructors"
-        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
+       C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
+       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
+	 fo_unif_subst_exp_named_subst
+	   test_equality_only 
+	   subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
+       else
+	 raise (UnificationFailure "5")
+	   (* (sprintf
+              "Can't unify %s with %s due to different inductive constructors"
+              (CicMetaSubst.ppterm subst t1) 
+	      (CicMetaSubst.ppterm subst t2))) *)
    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
                               subst context metasenv te t2 ugraph
@@ -583,96 +459,78 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
        fo_unif_subst 
         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
    | (C.Appl l1, C.Appl l2) -> 
-(* WAS BEFORE ----------
-       let subst,metasenv,t1',t2',ugraph1 =
-        match l1,l2 with
-           C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j ->
-             subst,metasenv,t1,t2,ugraph
-         (* In the first two cases when we reach the next begin ... end
-            section useless work is done since, by construction, the list
-            of arguments will be equal.
-         *)
------------------ *)
        (* andrea: this case should be probably rewritten in the 
 	  spirit of deref *)
-       let rec beta_reduce =
-         function
-             (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-               let he'' = CicSubstitution.subst he' t in
-                 if tl' = [] then
-                   he''
-                 else
-                   beta_reduce (Cic.Appl(he''::tl'))
-           | t -> t in
-	let exists_a_meta l = 
-	     List.exists (function Cic.Meta _ -> true | _ -> false) l
-	in
-        (match l1,l2 with
-           C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
-             (try 
-		List.fold_left2 
-		 (fun (subst,metasenv,ugraph) t1 t2 ->
-		    fo_unif_subst 
-		      test_equality_only subst context metasenv t1 t2 ugraph)
-		  (subst,metasenv,ugraph) l1 l2 
-	      with (Invalid_argument msg) -> raise (UnificationFailure msg)) 
-         | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
-	 (* we verify that none of the args is a Meta, since beta expanding 
-	    with respoect to a metavariable makes no sense 
-	  *)
-            (try 
-	       let (_,t,_) = CicUtil.lookup_subst i subst in
-	       let lifted = S.subst_meta l t in
-               let reduced = beta_reduce (Cic.Appl (lifted::args)) in
-	       fo_unif_subst 
-		 test_equality_only 
-		 subst context metasenv reduced t2 ugraph
-	     with CicUtil.Subst_not_found _ ->
-               let subst,metasenv,beta_expanded,ugraph1 =
-		 beta_expand_many 
-		   test_equality_only metasenv subst context t2 args ugraph 
-	       in
-                 fo_unif_subst test_equality_only subst context metasenv 
-		   (C.Meta (i,l)) beta_expanded ugraph1)
-         | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
-            (try 
-	       let (_,t,_) = CicUtil.lookup_subst i subst in
-	       let lifted = S.subst_meta l t in
-               let reduced = beta_reduce (Cic.Appl (lifted::args)) in
-	       fo_unif_subst 
-		 test_equality_only 
-		 subst context metasenv t1 reduced ugraph
-	     with CicUtil.Subst_not_found _ ->
-               let subst,metasenv,beta_expanded,ugraph1 =
-		 beta_expand_many 
-		   test_equality_only metasenv subst context t1 args ugraph in
-               fo_unif_subst test_equality_only subst context metasenv 
-		 (C.Meta (i,l)) beta_expanded ugraph1)
-         | _,_ ->
-	     let lr1 = List.rev l1 in
-             let lr2 = List.rev l2 in
-             let rec 
-               fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
-                 match (l1,l2) with
-                   [],_
-                 | _,[] -> assert false
-                 | ([h1],[h2]) ->
-                   fo_unif_subst 
-		       test_equality_only subst context metasenv h1 h2 ugraph
-                 | ([h],l) 
-                 | (l,[h]) ->
-                  fo_unif_subst test_equality_only subst context metasenv
-                    h (C.Appl (List.rev l)) ugraph
-                 | ((h1::l1),(h2::l2)) -> 
-                  let subst', metasenv',ugraph1 = 
-                   fo_unif_subst 
-		     test_equality_only subst context metasenv h1 h2 ugraph
-                  in 
-                   fo_unif_l 
-		     test_equality_only subst' metasenv' (l1,l2) ugraph1
-             in
-               fo_unif_l 
-		 test_equality_only subst metasenv (lr1, lr2)  ugraph)(**)
+       (match l1,l2 with
+          | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
+	      (try 
+		 List.fold_left2 
+		   (fun (subst,metasenv,ugraph) t1 t2 ->
+		      fo_unif_subst 
+			test_equality_only subst context metasenv t1 t2 ugraph)
+		   (subst,metasenv,ugraph) l1 l2 
+	       with (Invalid_argument msg) -> 
+		 raise (UnificationFailure msg)) 
+          | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
+	      (* we verify that none of the args is a Meta, 
+                since beta expanding with respoect to a metavariable 
+                makes no sense  *)
+ (*
+              (try 
+		 let (_,t,_) = CicUtil.lookup_subst i subst in
+		 let lifted = S.subst_meta l t in
+		 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+		   fo_unif_subst 
+		    test_equality_only 
+		     subst context metasenv reduced t2 ugraph
+	       with CicUtil.Subst_not_found _ -> *)
+	      let subst,metasenv,beta_expanded,ugraph1 =
+		beta_expand_many 
+		  test_equality_only metasenv subst context t2 args ugraph 
+	      in
+                fo_unif_subst test_equality_only subst context metasenv 
+		  (C.Meta (i,l)) beta_expanded ugraph1
+          | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
+              (* (try 
+		 let (_,t,_) = CicUtil.lookup_subst i subst in
+		 let lifted = S.subst_meta l t in
+		 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+		   fo_unif_subst 
+		     test_equality_only 
+		     subst context metasenv t1 reduced ugraph
+	       with CicUtil.Subst_not_found _ -> *)
+		 let subst,metasenv,beta_expanded,ugraph1 =
+		   beta_expand_many 
+		     test_equality_only 
+		     metasenv subst context t1 args ugraph in
+		   fo_unif_subst test_equality_only subst context metasenv 
+		     (C.Meta (i,l)) beta_expanded ugraph1
+          | _,_ ->
+	      let lr1 = List.rev l1 in
+              let lr2 = List.rev l2 in
+              let rec 
+		  fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
+                match (l1,l2) with
+                    [],_
+                  | _,[] -> assert false
+                  | ([h1],[h2]) ->
+                      fo_unif_subst 
+			test_equality_only subst context metasenv h1 h2 ugraph
+                  | ([h],l) 
+                  | (l,[h]) ->
+                      fo_unif_subst test_equality_only subst context metasenv
+			h (C.Appl (List.rev l)) ugraph
+                  | ((h1::l1),(h2::l2)) -> 
+                      let subst', metasenv',ugraph1 = 
+			fo_unif_subst 
+			  test_equality_only 
+			  subst context metasenv h1 h2 ugraph
+                      in 
+			fo_unif_l 
+			  test_equality_only subst' metasenv' (l1,l2) ugraph1
+              in
+		fo_unif_l 
+		  test_equality_only subst metasenv (lr1, lr2)  ugraph)
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
@@ -690,15 +548,18 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
          Invalid_argument _ ->
           raise (UnificationFailure "6"))
            (* (sprintf
-            "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) *)
+              "Error trying to unify %s with %s: the number of branches is not the same." 
+	      (CicMetaSubst.ppterm subst t1) 
+	      (CicMetaSubst.ppterm subst t2)))) *)
    | (C.Rel _, _) | (_,  C.Rel _) ->
        if t1 = t2 then
          subst, metasenv,ugraph
        else
         raise (UnificationFailure "6")
           (* (sprintf
-          "Can't unify %s with %s because they are not convertible"
-          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
+             "Can't unify %s with %s because they are not convertible"
+             (CicMetaSubst.ppterm subst t1) 
+	     (CicMetaSubst.ppterm subst t2))) *)
    | (C.Sort _ ,_) | (_, C.Sort _)
    | (C.Const _, _) | (_, C.Const _)
    | (C.MutInd  _, _) | (_, C.MutInd _)
@@ -714,11 +575,25 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 	   if b then 
 	     subst, metasenv, ugraph1
 	   else
-             raise (UnificationFailure "7")
-               (* (sprintf
+             raise (* (UnificationFailure "7") *)
+                (UnificationFailure (sprintf
 		  "Can't unify %s with %s because they are not convertible"
 		  (CicMetaSubst.ppterm subst t1) 
-		  (CicMetaSubst.ppterm subst t2))) *)
+		  (CicMetaSubst.ppterm subst t2)))
+   | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
+       let subst,metasenv,beta_expanded,ugraph1 =
+	 beta_expand_many 
+	   test_equality_only metasenv subst context t2 args ugraph 
+       in
+         fo_unif_subst test_equality_only subst context metasenv 
+	   (C.Meta (i,l)) beta_expanded ugraph1
+   | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
+       let subst,metasenv,beta_expanded,ugraph1 =
+	 beta_expand_many 
+	   test_equality_only metasenv subst context t1 args ugraph 
+       in
+         fo_unif_subst test_equality_only subst context metasenv 
+	   beta_expanded (C.Meta (i,l)) ugraph1
    | (C.Prod _, t2) ->
        let t2' = R.whd ~subst context t2 in
        (match t2' with
@@ -732,7 +607,12 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 	    C.Prod _ -> 
 	      fo_unif_subst test_equality_only 
 		subst context metasenv t1' t2 ugraph	 
-	  | _ -> raise (UnificationFailure "9"))
+	  | _ -> (* raise (UnificationFailure "9")) *)
+              raise 
+		(UnificationFailure (sprintf
+		   "Can't unify %s with %s because they are not convertible"
+		   (CicMetaSubst.ppterm subst t1) 
+		   (CicMetaSubst.ppterm subst t2))))
    | (_,_) ->
        let b,ugraph1 = 
 	 R.are_convertible ~subst ~metasenv context t1 t2 ugraph