From d556d11bb205b101c9dfa20f35fdd1b0be1ae3a8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 29 Apr 2002 10:07:47 +0000 Subject: [PATCH] Bug fixed: the unwinding was not recursively performed. (a "t" should have been a "t'") --- helm/ocaml/cic_unification/cicUnification.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index a01f9a9b8..ce7aa5280 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -202,11 +202,11 @@ let unwind subst unwinded t = try let t = List.assoc i subst in let t' = um_aux 0 t in - unwinded := (i,t)::!unwinded ; + unwinded := (i,t')::!unwinded ; S.lift k t' with Not_found -> - (* not constrained variable, i.e. free in subst *) + (* not constrained variable, i.e. free in subst*) C.Meta i in frozen := saved_frozen ; @@ -334,10 +334,6 @@ let apply_subst_reducing subst meta_to_reduce t = ;; (* UNWIND THE MGU INSIDE THE MGU *) -(* let unwind mgu = - let mark = Array.make (Array.length mgu) 0 in - Array.iter (fun x -> let foo = unwind_meta mgu mark x in ()) mgu; mgu;; *) - let unwind_subst subst = List.fold_left (fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst -- 2.39.2