From f6f4161c5a535bd92de2faced020a41d0c6a304d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 Aug 2007 09:39:34 +0000 Subject: [PATCH] Avoid reusing Hbeta several times. --- .../components/cic_unification/cicUnification.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) 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 -- 2.39.2