X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=ace3c80a4b3e58be099dcd4fb1bff0cd5d155fb4;hb=2b5892c042136ebb0d9a2f773f3174c840ca0ba6;hp=a41e2fb349f0cb31b39ceda6f463116c64324e7b;hpb=824a3ed3852a6a87c59373efb3ebde145de2a757;p=helm.git

diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml
index a41e2fb34..ace3c80a4 100644
--- a/matita/components/ng_tactics/nCicElim.ml
+++ b/matita/components/ng_tactics/nCicElim.ml
@@ -116,7 +116,7 @@ let mk_elim status uri leftno it (outsort,suffix) pragma =
    ) cl
  in
  let branches, branch_args = List.split branches_with_args in
- let bo = NotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in
+ let bo = NotationPt.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] @
@@ -225,9 +225,7 @@ let pp (status: #NCic.status) =
  let rec pp rels =
   function
     NCic.Rel i -> List.nth rels (i - 1)
-  | NCic.Const _ as t ->
-     NotationPt.Ident
-      (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
+  | NCic.Const _ as t -> NotationPt.NCic t
   | NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s))
   | NCic.Meta _
   | NCic.Implicit _ -> assert false