proof simplified

[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 106d92706e8fbe7e46783fb0f0d9cca12353ee21..57f130546d9ed4c5a663e88119fba719d6df2e7f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -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) =