working version

[helm.git] / matita / components / ng_tactics / nCicElim.ml

diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml
index a41e2fb349f0cb31b39ceda6f463116c64324e7b..5a264c403076220a3a861b8049325224e0def47f 100644 (file)
--- 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] @
@@ -166,9 +166,9 @@ let mk_elim status uri leftno it (outsort,suffix) pragma =
      (function x::_ -> x | _ -> assert false) 80 
      (NotationPres.mpres_of_box boxml)));
 *)
+  let attrs = `Generated, `Definition, pragma in
   NotationPt.Theorem
-   (`Definition,srec_name,
-      NotationPt.Implicit `JustOne,Some res,pragma)
+   (srec_name, NotationPt.Implicit `JustOne, Some res, attrs)
 ;;
 
 let ast_of_sort s =
@@ -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
@@ -238,7 +236,7 @@ let pp (status: #NCic.status) =
   | NCic.Lambda (n,s,t) ->
      let n = mk_id n in
       NotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t)
-  | NCic.LetIn (n,s,ty,t) ->
+  | NCic.LetIn (n,ty,s,t) ->
      let n = mk_id n in
       NotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t)
   | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
@@ -310,8 +308,9 @@ let mk_projection status leftno tyname consname consty (projname,_,_) i =
      (function x::_ -> x | _ -> assert false)
      80 (NotationPres.render (fun _ -> None)
      (TermContentPres.pp_ast res)));*)
+  let attrs = `Generated, `Definition, `Projection in
   NotationPt.Theorem
-   (`Definition,projname,NotationPt.Implicit `JustOne,Some res,`Projection)
+   (projname, NotationPt.Implicit `JustOne, Some res, attrs)
 ;;
 
 let mk_projections status (_,_,_,_,obj) =