From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 19:28:48 +0000 (+0000)
Subject: More info to refine empty types elimination.
X-Git-Tag: make_still_working~3662
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=24c5f3d919918175b6380f47cf9613ee4bd7af80;p=helm.git

More info to refine empty types elimination.
---

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 1401ed48f..ae472ae38 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -109,7 +109,7 @@ let mk_elim uri leftno [it] (outsort,suffix) =
        mk_appl (name_of_k name :: cargs @ recursive_args)
    ) cl
  in
- let bo = CicNotationPt.Case (rec_arg,None,None,branches) in
+ let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in
  let recno = List.length final_params in
  let where = recno - 1 in
  let res =