From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 29 Nov 2004 12:24:25 +0000 (+0000)
Subject: passes subst to FreshNameGenerator
X-Git-Tag: PRE_UNIVERSES~6
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=887340c4bccbc9f83dda7bb99c9d929852d9d1a9;p=helm.git

passes subst to FreshNameGenerator
---

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 63abdfb01..c88e6b78d 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -207,7 +207,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
   in
   let argty = type_of_aux' metasenv subst context arg in
   let fresh_name =
-   FreshNamesGenerator.mk_fresh_name
+   FreshNamesGenerator.mk_fresh_name ~subst
     metasenv context (Cic.Name "Heta") ~typ:argty
   in
    let subst,metasenv,t' = aux metasenv subst 0 context t in