passes subst to FreshNameGenerator

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 63abdfb012a2dca27af1e9eaa11d022aca63c0a9..c88e6b78d5fc62fdbf3fd995be9920d102f5b038 100644 (file)
--- 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