Bug fixed: the beta_expansion function did not lift the argument before

attempting to match it ==> no matching was done correctly under an
abstraction.

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index c8ed004775bdf9d86dfd61fbbe1cdd408864ded0..646670ec8425ca3a55a467e59956f3967e923fb0 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -49,7 +49,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
   let rec aux metasenv subst n context t' =
    try
     let subst,metasenv =
-     fo_unif_subst test_equality_only subst context metasenv arg t'
+     fo_unif_subst test_equality_only subst context metasenv
+      (CicSubstitution.lift n arg) t'
     in
      subst,metasenv,C.Rel (1 + n)
    with