From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 5 Feb 2004 14:38:56 +0000 (+0000)
Subject: "assert false" relaxed to a warning.
X-Git-Tag: V_0_2_3~40
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1c04fd27caa8bfb794848c90202bbc65b29c0cfa;p=helm.git

"assert false" relaxed to a warning.
The problem raises when a non-dependent type is found and there IS a Rel
to it. It used to be an assert false (that failed). It is now relaxed
to a Cic.Anonymous (plus a warning on stderr).
---

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