X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=0abff3a6c694727f79cc2e07eded3fd6ce48cc82;hb=d34061fd1c820139fad38c39dee6377e5057bf26;hp=4339b2860f42531eef867c1860a5536e0b44e586;hpb=ee7855524284ea3a282c68f22ffa36e535a11810;p=helm.git

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 4339b2860..0abff3a6c 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -98,7 +98,7 @@ let mk_elim uri leftno [it] (outsort,suffix) =
                       params @
                       [p_name] @
                       k_names @
-                      List.map (fun _ -> CicNotationPt.Implicit)
+                      List.map (fun _ -> CicNotationPt.Implicit `JustOne)
                        (List.tl args) @
                       [mk_appl (name::abs)])))
               | _ -> mk_id name,None
@@ -148,7 +148,8 @@ let mk_elim uri leftno [it] (outsort,suffix) =
      (function x::_ -> x | _ -> assert false) 80 
      (CicNotationPres.mpres_of_box boxml)));
 *)
-  CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res)
+  CicNotationPt.Theorem
+   (`Definition,srec_name,CicNotationPt.Implicit `JustOne,Some res)
 ;;
 
 let ast_of_sort s =
@@ -280,7 +281,8 @@ let mk_projection leftno tyname consname consty (projname,_,_) i =
      (function x::_ -> x | _ -> assert false)
      80 (CicNotationPres.render (fun _ -> None)
      (TermContentPres.pp_ast res)));*)
-  CicNotationPt.Theorem (`Definition,projname,CicNotationPt.Implicit,Some res)
+  CicNotationPt.Theorem
+   (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res)
 ;;
 
 let mk_projections (_,_,_,_,obj) =