From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 5 Jul 2004 07:12:30 +0000 (+0000)
Subject: Bug fixed: beta_expand did not perform any recursion over the local context
X-Git-Tag: pre_subst_in_kernel~6
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3db0a84a64f014fa10c4b439c62cb3eef017ea7a;p=helm.git

Bug fixed: beta_expand did not perform any recursion over the local context
of a metavariable ==> the local context was not lifted.
---

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 646670ec8..e6213d6af 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -67,8 +67,20 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
            (try
              let (_, t') = CicMetaSubst.lookup_subst i subst in
               aux metasenv subst n context (CicSubstitution.lift_meta l t')
-            with
-             CicMetaSubst.SubstNotFound _ -> subst,metasenv,t)
+            with CicMetaSubst.SubstNotFound _ ->
+              let (subst, metasenv, context, local_context) =
+                List.fold_left
+                  (fun (subst, metasenv, context, local_context) t ->
+                    match t with
+                    | None -> (subst, metasenv, context, None :: local_context)
+                    | Some t ->
+                        let (subst, metasenv, t) =
+                          aux metasenv subst n context t
+                        in
+                        (subst, metasenv, context, Some t :: local_context))
+                  (subst, metasenv, context, []) l
+              in
+              (subst, metasenv, C.Meta (i, local_context)))
         | C.Sort _
         | C.Implicit _ as t -> subst,metasenv,t
         | C.Cast (te,ty) ->
@@ -387,8 +399,8 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
                    fo_unif_subst test_equality_only subst context metasenv h1 h2
                | ([h],l) 
                | (l,[h]) ->
-                  fo_unif_subst 
-	           test_equality_only subst context metasenv h (C.Appl (List.rev l))
+                  fo_unif_subst test_equality_only subst context metasenv
+                    h (C.Appl (List.rev l))
                | ((h1::l1),(h2::l2)) -> 
                   let subst', metasenv' = 
                    fo_unif_subst test_equality_only subst context metasenv h1 h2