X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_kernel%2FnCicUtils.ml;h=400d693638f880366da93bffe5b187b24eea2933;hb=e79c8b830f9f6b0c3f4d577909e32e1bb4032cdf;hp=f22e02a7eaa1da016bc202e3afa4793578eec86a;hpb=9dac2c325dca1b5b92d6ba11dadf470538bae28e;p=helm.git

diff --git a/matitaB/components/ng_kernel/nCicUtils.ml b/matitaB/components/ng_kernel/nCicUtils.ml
index f22e02a7e..400d69363 100644
--- a/matitaB/components/ng_kernel/nCicUtils.ml
+++ b/matitaB/components/ng_kernel/nCicUtils.ml
@@ -17,7 +17,7 @@ module Ref = NReference
 exception Subst_not_found of int
 exception Meta_not_found of int
 
-let head_beta_reduce = ref (fun _ ~upto:_ _ -> assert false);;
+let head_beta_reduce = ref (fun (_:NCicEnvironment.status) ~upto:_ _ -> assert false);;
 let set_head_beta_reduce = (:=) head_beta_reduce;;
 
 let expand_local_context = function
@@ -74,7 +74,7 @@ let map status g k f = function
       | C.Appl l :: tl -> C.Appl (l@tl)
       | l1 -> C.Appl l1
     in
-      if fire_beta then !head_beta_reduce (status :> NCic.status) ~upto t
+      if fire_beta then !head_beta_reduce (status :> NCicEnvironment.status) ~upto t
       else t
  | C.Prod (n,s,t) as orig ->
      let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in