X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;fp=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;h=3bdde5b593426125143aa874e904feb1069d1e4b;hb=a785a3526d4dcbb6c5810ed4fb943132c9ff2d45;hp=1a94c318599e2678e0898618d1fe40c254653d4b;hpb=38633ee024797543bba347addb8f287fd3e5331f;p=helm.git

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 1a94c3185..3bdde5b59 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -27,14 +27,14 @@
 (* returns an identifier which is fresh in the context *)
 (* and that resembles [name] as much as possible.      *)
 (* [typ] will be the type of the variable              *)
-let mk_fresh_name metasenv context name ~typ =
+let mk_fresh_name ~subst metasenv context name ~typ =
  let module C = Cic in
   let basename =
    match name with
       C.Anonymous ->
        (*CSC: great space for improvements here *)
        (try
-         (match CicTypeChecker.type_of_aux' metasenv context typ with
+         (match CicTypeChecker.type_of_aux' ~subst metasenv context typ with
              C.Sort C.Prop
            | C.Sort C.CProp -> "H"
            | C.Sort C.Set -> "x"