- changed license to lgpl

[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 371ca99fa323e31d1873df3c68b843ef4f135989..036ba07a94a6c2fdea4526577741faafd73b6305 100644 (file)
--- a/helm/ocaml/cic_unification/freshNamesGenerator.mli
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli
@@ -28,4 +28,11 @@
 (* 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 *)
+(* 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