X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.mli;h=036ba07a94a6c2fdea4526577741faafd73b6305;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=02acf9b03f130e28026875538a9574f7574e2875;hpb=d8a1a68b8b7e53ba43fcad55e928a99ef5e08b8e;p=helm.git

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli
index 02acf9b03..036ba07a9 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.mli
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli
@@ -28,7 +28,8 @@
 (* and that resembles [name] as much as possible.      *)
 (* [typ] will be the type of the variable              *)
 val mk_fresh_name :
- Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+  subst:Cic.substitution ->
+  Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
 
 (* clean_dummy_dependent_types term                               *)
 (* returns a copy of [term] where every dummy dependent product *)