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 646670ec8425ca3a55a467e59956f3967e923fb0..e6213d6af8895d0b0cc3c1ea6a726b18eec00e8d 100644 (file)
--- 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