This commit patches the environment and the library so that their status is

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

diff --git a/matitaB/components/ng_tactics/nCicElim.ml b/matitaB/components/ng_tactics/nCicElim.ml
index c2543711a5d40ce53ad10eecb162e9ece4704644..fd20de1dcb6eb9aba3ec4531eaa921157821c6bf 100644 (file)
--- 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))
    | _ -> []
 ;;