From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Aug 2007 09:39:34 +0000 (+0000)
Subject: Avoid reusing Hbeta several times.
X-Git-Tag: make_still_working~6108
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f6f4161c5a535bd92de2faced020a41d0c6a304d;p=helm.git

Avoid reusing Hbeta several times.
---

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 912ae1e8e..fb6a66d4f 100644
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -136,7 +136,7 @@ let eta_reduce after_beta_expansion after_beta_expansion_body
  with
   WrongShape -> after_beta_expansion
 
-let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
+let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
  let module S = CicSubstitution in
  let module C = Cic in
 let foo () =
@@ -279,7 +279,7 @@ let foo () =
   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
   let fresh_name =
    FreshNamesGenerator.mk_fresh_name ~subst
-    metasenv context (Cic.Name "Hbeta") ~typ:argty
+    metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
   in
    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
@@ -288,15 +288,15 @@ in profiler_beta_expand.HExtlib.profile foo ()
 
 
 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
-  let subst,metasenv,hd,ugraph =
+  let _,subst,metasenv,hd,ugraph =
     List.fold_right
-      (fun arg (subst,metasenv,t,ugraph) ->
+      (fun arg (num,subst,metasenv,t,ugraph) ->
          let subst,metasenv,t,ugraph1 =
-           beta_expand test_equality_only 
+           beta_expand num test_equality_only 
              metasenv subst context t arg ugraph 
          in
-           subst,metasenv,t,ugraph1 
-      ) args (subst,metasenv,t,ugraph) 
+           num+1,subst,metasenv,t,ugraph1 
+      ) args (1,subst,metasenv,t,ugraph) 
   in
     subst,metasenv,hd,ugraph