debruijn simplified. It could go in nCicUtils, but why should we do that?

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 2f8f69a41b8b77b1e629b0ea683a395bddba74cc..7995f5c8720e5903501b2e5fa22424c0b91182bc 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -102,20 +102,17 @@ let rec split_prods ~subst context n te =
    | (_, _) -> raise (AssertFailure (lazy "split_prods"))
 ;;
 
-let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context = 
+let debruijn uri number_of_types context = 
  let rec aux k t =
-  let res =
-   match t with
-    | C.Meta (i,(s,C.Ctx l)) ->
-       let l1 = HExtlib.sharing_map (aux (k-s)) l in
-       if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
-    | C.Meta _ -> t
-    | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) 
-    | C.Const (Ref.Ref (_,uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
-       C.Rel (k + number_of_types - no)
-    | t -> U.map (fun _ k -> k+1) k aux t
-  in
-   cb t res; res
+  match t with
+   | C.Meta (i,(s,C.Ctx l)) ->
+      let l1 = HExtlib.sharing_map (aux (k-s)) l in
+      if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
+   | C.Meta _ -> t
+   | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) 
+   | C.Const (Ref.Ref (_,uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
+      C.Rel (k + number_of_types - no)
+   | t -> U.map (fun _ k -> k+1) k aux t
  in
   aux (List.length context)
 ;;