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 1401ed48f8b6ecc7fe9849e02496a8fb62428031..ae472ae38cbdaf37633b73fe2655342d589fa1bc 100644 (file)
--- 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 =