X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;fp=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;h=fc1b4f36e7c5cabf9efe6c992dedf428087e573e;hb=1c04fd27caa8bfb794848c90202bbc65b29c0cfa;hp=80a26888f320b0e10a2a1723715fe1f52a0c75f2;hpb=a8c20c4385d6045b848d21af9f30fc583de2aaa2;p=helm.git

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 80a26888f..fc1b4f36e 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -106,7 +106,13 @@ let clean_dummy_dependent_types t =
         let n' =
          match n with
             C.Anonymous ->
-             if List.mem k rels2 then assert false else C.Anonymous
+             if List.mem k rels2 then
+(
+              prerr_endline "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
+              C.Anonymous
+)
+             else
+              C.Anonymous
           | C.Name _ as n ->
              if List.mem k rels2 then n else C.Anonymous
         in