X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=fd20de1dcb6eb9aba3ec4531eaa921157821c6bf;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=0840b16a65718f6bb77f71dfb2e92b02dadd9e7e;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git

diff --git a/matitaB/components/ng_tactics/nCicElim.ml b/matitaB/components/ng_tactics/nCicElim.ml
index 0840b16a6..fd20de1dc 100644
--- a/matitaB/components/ng_tactics/nCicElim.ml
+++ b/matitaB/components/ng_tactics/nCicElim.ml
@@ -197,7 +197,7 @@ let mk_elims status (uri,_,_,_,obj) =
     NCic.Inductive (true,leftno,[itl],_) ->
       List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s))
        (NCic.Prop::
-         List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+         List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes status))
    | _ -> []
 ;;
 
@@ -225,10 +225,7 @@ let pp (status: #NCic.status) =
  let rec pp rels =
   function
     NCic.Rel i -> List.nth rels (i - 1)
-  | NCic.Const r as t ->
-     NotationPt.Ident
-      (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,
-       `Uri (NReference.string_of_reference r))
+  | NCic.Const _ as t -> NotationPt.NCic t
   | NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s))
   | NCic.Meta _
   | NCic.Implicit _ -> assert false