X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=5a264c403076220a3a861b8049325224e0def47f;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=95b8f783d745df349fa19ac0da270dea74cb1189;hpb=225887a9f23aac79d4cca907da026917b7df04dc;p=helm.git

diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml
index 95b8f783d..5a264c403 100644
--- a/matita/components/ng_tactics/nCicElim.ml
+++ b/matita/components/ng_tactics/nCicElim.ml
@@ -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 =
@@ -308,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) =