X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=359d93bbd5c72c48ff5700060fb82c4935ce0026;hb=23fa9e70972efb0a805a4fecf6c91103f42408f2;hp=4d32c197d88fa2a71416d3a15812dc9eaecce7e5;hpb=ec73d44deba0365d258df455b0bd04ae1764cf76;p=helm.git

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 4d32c197d..359d93bbd 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -116,7 +116,7 @@ let mk_elim uri leftno it (outsort,suffix) pragma =
    ) cl
  in
  let branches, branch_args = List.split branches_with_args in
- let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in
+ let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),Some p_name,branches) in
  let final_params =
   List.map (function name -> name, None) params @
   [p_name,Some p_ty] @