fresh_name_generator has now also the metasenv parameter.

[helm.git] / helm / ocaml / cic_unification / freshNamesGenerator.mli

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli
index e350363e9d7e624d15a7cc96fed72c5ad07078d2..371ca99fa323e31d1873df3c68b843ef4f135989 100644 (file)
--- a/helm/ocaml/cic_unification/freshNamesGenerator.mli
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli
@@ -23,8 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* mk_fresh_name context name typ                      *)
+(* mk_fresh_name metasenv context name typ             *)
 (* 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              *)
-val mk_fresh_name : Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+val mk_fresh_name :
+ Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name