first moogle template checkin

[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..1a94c318599e2678e0898618d1fe40c254653d4b 100644 (file)
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -95,7 +95,7 @@ let clean_dummy_dependent_types t =
        in
         C.Meta(i,l'),rels
     | C.Sort _ as t -> t,[]
-    | C.Implicit as t -> t,[]
+    | C.Implicit _ as t -> t,[]
     | C.Cast (te,ty) ->
        let te',rels1 = aux k te in
        let ty',rels2 = aux k ty in
@@ -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