"assert false" relaxed to a warning.

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

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 80a26888f320b0e10a2a1723715fe1f52a0c75f2..fc1b4f36e7c5cabf9efe6c992dedf428087e573e 100644 (file)
--- 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