X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.mli;h=02acf9b03f130e28026875538a9574f7574e2875;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=371ca99fa323e31d1873df3c68b843ef4f135989;hpb=feb3c287997f7d35747c12e0db62e6194f5587a3;p=helm.git

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli
index 371ca99fa..02acf9b03 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.mli
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli
@@ -29,3 +29,9 @@
 (* [typ] will be the type of the variable              *)
 val mk_fresh_name :
  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