fixed some regressions

[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.ml

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index bd0587a43a53f3fd6afb5f8dda9954167c9716f1..57f130546d9ed4c5a663e88119fba719d6df2e7f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -19,7 +19,7 @@ exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t;;
 exception BadConstraint of string Lazy.t;;
 
-let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+let type0 = []
 
 let le_constraints = ref [] (* strict,a,b *)
 
@@ -152,12 +152,12 @@ let get_checked_indtys = function
 ;;
 
 let get_checked_fixes_or_cofixes = function
-  | Ref.Ref (uri, (Ref.Fix (fixno,_,_)|Ref.CoFix fixno))->
+  | Ref.Ref (uri, (Ref.Fix _|Ref.CoFix _))->
       (match get_checked_obj uri with
       | _,height,_,_, C.Fixpoint (_,funcs,att) ->
          funcs, att, height
       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
-  | r -> prerr_endline ("get_checked_(co)fix on " ^ Ref.string_of_reference r); assert false
+  | _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false
 ;;
 
 let get_relevance (Ref.Ref (_, infos) as r) =