From 9a10854931b9271c215040533a65e5330bc75122 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Jul 2004 15:18:06 +0000 Subject: [PATCH] Bug fixed: the beta_expansion function did not lift the argument before attempting to match it ==> no matching was done correctly under an abstraction. --- helm/ocaml/cic_unification/cicUnification.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index c8ed00477..646670ec8 100644 --- 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 -- 2.39.2