From f6f4161c5a535bd92de2faced020a41d0c6a304d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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.5