Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml.

This is to move a standard combinator to the place it belongs to. An
alternative could have been to put it in termops.ml, but termops.ml is
now about econstr, so, even if it makes the kernel "bigger", constr.ml
seems to be the best place for this combinator. After all, this
combinator is canonical.

4 files changed, 32 insertions, 43 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index efe1525c9a..13bd8f7718 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -816,26 +816,11 @@ let map_constr_with_full_binders_user_view sigma g f =
    each binder traversal; it is not recursive *)
 
 let fold_constr_with_full_binders sigma g f n acc c =
-  let open RelDecl in
-  match EConstr.kind sigma c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> acc
-  | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c
-  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
-  | Proj (p,c) -> f n acc c
-  | Evar (_,l) -> Array.fold_left (f n) acc l
-  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
-  | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
-      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
-      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
-  | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
-      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
-      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  let open EConstr in
+  let f l acc c = f l acc (of_constr c) in
+  let g d l  = g (of_rel_decl d) l in
+  let c = Unsafe.to_constr (whd_evar sigma c) in
+  Constr.fold_with_full_binders g f n acc c
 
 let fold_constr_with_binders sigma g f n acc c =
   fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c97969c0e0..557ed2caa8 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -440,6 +440,27 @@ let fold f acc c = match kind c with
   | CoFix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
 
+let fold_with_full_binders g f n acc c =
+  let open Context.Rel.Declaration in
+  match kind c with
+  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _ -> acc
+  | Cast (c,_, t) -> f n (f n acc c) t
+  | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+  | Proj (_,c) -> f n acc c
+  | Evar (_,l) -> Array.fold_left (f n) acc l
+  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+  | Fix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | CoFix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+
 (* [iter f c] iters [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 3c9cc96a0d..d97afffc53 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -465,6 +465,10 @@ val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Decla
 
 val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 
+val fold_with_full_binders :
+  (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
+    'a -> 'b -> constr -> 'b
+
 (** [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 15c0278f47..6beac2032d 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -162,27 +162,6 @@ let label_of = function
   | ConstructRef ((kn,_),_) -> MutInd.label kn
   | VarRef id -> Label.of_id id
 
-let fold_constr_with_full_binders g f n acc c =
-  let open Context.Rel.Declaration in
-  match Constr.kind c with
-  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _ -> acc
-  | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
-  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
-  | Proj (p,c) -> f n acc c
-  | Evar (_,l) -> Array.fold_left (f n) acc l
-  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
-  | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
-      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
-      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
-  | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
-      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
-      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
-
 let rec traverse current ctx accu t = match Constr.kind t with
 | Var id ->
   let body () = id |> Global.lookup_named |> NamedDecl.get_value in
@@ -205,10 +184,10 @@ let rec traverse current ctx accu t = match Constr.kind t with
         traverse_object
           ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
     | _ ->
-        fold_constr_with_full_binders
+        Constr.fold_with_full_binders
           Context.Rel.add (traverse current) ctx accu t
     end
-| _ -> fold_constr_with_full_binders
+| _ -> Constr.fold_with_full_binders
           Context.Rel.add (traverse current) ctx accu t
 
 and traverse_object ?inhabits (curr, data, ax2ty) body obj =