X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.mli;h=036ba07a94a6c2fdea4526577741faafd73b6305;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=e350363e9d7e624d15a7cc96fed72c5ad07078d2;hpb=7b922ad1f9832c1edb3acea8f0c910fa2c0c20e5;p=helm.git

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli
index e350363e9..036ba07a9 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.mli
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli
@@ -23,8 +23,16 @@
  * 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 :
+  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 *)
+(* have been replaced with a non-dependent product and where    *)
+(* dummy let-ins have been removed.                             *)
+val clean_dummy_dependent_types : Cic.term -> Cic.term