From 4d08e8112264c289fdcc978ee81d9352e972edcf Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 22 Apr 2004 12:33:35 +0000
Subject: [PATCH] Big bug fixed: in the case  t <?= ?1, the instantiation ?1 :=
 t was generated and then t : C and ?1 : E were retrieved/computed correctly;
 then E <?= T was incorrectly tested (instead of T <?= E).

---
 helm/ocaml/cic_unification/cicUnification.ml | 24 +++++++++-----------
 1 file changed, 11 insertions(+), 13 deletions(-)

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index c56fb0874..b9f87cf9a 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -96,24 +96,22 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
        fo_unif_subst subst context metasenv t2 t1
    | (C.Meta (n,l), t)   
    | (t, C.Meta (n,l)) ->
-       let fo_unif_subst =
-        let (lower,upper) =
-         match t1,t2 with
-            C.Meta (n,_), C.Meta (m,_) when n < m ->
-             (fun t1 t2 -> t1), (fun t1 t2 -> t2)
-          | _, C.Meta _ ->
-             (fun t1 t2 -> t1), (fun t1 t2 -> t2)
-          | _,_ ->
-             (fun t1 t2 -> t2), (fun t1 t2 -> t1)
-        in
-         fun subst context metasenv m1 m2 ->
+       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 subst context metasenv m1 m2 =
           fo_unif_subst subst context metasenv (lower m1 m2) (upper m1 m2)
        in
        let subst'',metasenv' =
         try
          let oldt = (List.assoc n subst) in
          let lifted_oldt = S.lift_meta l oldt in
-          fo_unif_subst subst context metasenv t lifted_oldt
+          fo_unif_subst_ordered subst context metasenv t lifted_oldt
         with Not_found ->
          let t',metasenv',subst' =
           try
@@ -122,7 +120,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
              (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
            | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
          in
-          (n, t')::subst', metasenv'
+	  (n, t')::subst', metasenv'
        in
         let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
         (try
-- 
2.39.2