X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;h=fc1b4f36e7c5cabf9efe6c992dedf428087e573e;hb=d7d9d42a3d44ff82f797bd36c3a0ccc05f48483d;hp=3664b4a72473008ec526a83049df98ae0922b340;hpb=d8a1a68b8b7e53ba43fcad55e928a99ef5e08b8e;p=helm.git

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 3664b4a72..fc1b4f36e 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -69,7 +69,7 @@ let clean_dummy_dependent_types t =
  let module C = Cic in
   let rec aux k =
    function
-      C.Rel m as t -> t,[m - k]
+      C.Rel m as t -> t,[k - m]
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst',rels = 
         List.fold_right
@@ -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