From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 29 Apr 2002 10:07:47 +0000 (+0000)
Subject: Bug fixed: the unwinding was not recursively performed. (a "t" should have been
X-Git-Tag: V_0_3_0_debian_8~120
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d556d11bb205b101c9dfa20f35fdd1b0be1ae3a8;p=helm.git

Bug fixed: the unwinding was not recursively performed. (a "t" should have been
a "t'")
---

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