- we are moving from old (patched) management of sort inclusion

[helm.git] / helm / software / helena / src / basic_rg / brgValidity.ml

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index ea3ce2f42b40e90f647fe608cdd092881b6f30b5..458962b1f5aa69c31365a4dcb0b082afe10924eb 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -12,7 +12,6 @@
 module L  = Log
 module G  = Options
 module E  = Entity
-module S  = Status
 module B  = Brg
 module BE = BrgEnvironment
 module BR = BrgReduction
@@ -62,7 +61,7 @@ let assert_applicability err f st m v t =
       | _                                -> assert false (**)
 
 let rec b_validate err f st m x =
-   if !G.trace >= level then log1 st.S.lenv "Now checking" m x;
+   if !G.trace >= level then log1 st "Now checking" m x;
    match x with
    | B.Sort _         -> f ()
    | B.LRef (_, i)    ->