From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 11 Sep 2007 08:16:25 +0000 (+0000)
Subject: replaced an assert false that cause nat_ind not to be displayed with a dummy result
X-Git-Tag: make_still_working~6025
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=53c57446be6916c1f4c450e8a9de07f8448a26ae;p=helm.git

replaced an assert false that cause nat_ind not to be displayed with a dummy result
---

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index ddd1b5ebc..69a1f632d 100644
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -360,7 +360,7 @@ let infer_dependent ~headless context metasenv = function
                   (n <> Cic.Anonymous && fstorder src, t) :: 
                   aux (CicSubstitution.subst 
                         (Deannotate.deannotate_term t) tgt) tl
-              | _ -> assert false
+              | _ -> List.map (fun s -> false,s) (t::tl)
        in
        (false, he) :: aux hety tl
      with CicTypeChecker.TypeCheckerFailure _ -> assert false