Merge branch 'declarative' into matita-lablgtk3

[helm.git] / matita / components / ng_kernel / nCicUtils.ml

diff --git a/matita/components/ng_kernel/nCicUtils.ml b/matita/components/ng_kernel/nCicUtils.ml
index a99ae0407f638b65e2932239b6bafac51f13bc2e..398df307ed7202cadf92ecc843dd3d7b89a165ef 100644 (file)
--- a/matita/components/ng_kernel/nCicUtils.ml
+++ b/matita/components/ng_kernel/nCicUtils.ml
@@ -12,12 +12,11 @@
 (* $Id$ *)
 
 module C = NCic
-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 _ ~upto:_ _ -> assert false);;
 let set_head_beta_reduce = (:=) head_beta_reduce;;
 
 let expand_local_context = function
@@ -56,7 +55,7 @@ let fold g k f acc = function
  | C.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl
 ;;
 
-let map g k f = function
+let map status g k f = function
  | C.Meta _ -> assert false
  | C.Implicit _
  | C.Sort _
@@ -74,7 +73,7 @@ let map g k f = function
       | C.Appl l :: tl -> C.Appl (l@tl)
       | l1 -> C.Appl l1
     in
-      if fire_beta then !head_beta_reduce ~upto t
+      if fire_beta then !head_beta_reduce (status :> NCic.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