From a623c11adac7c34aae92dbeb0c5b7ecc863ce6fd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 6 Apr 2018 09:55:42 +0200
Subject: 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.
---
 engine/termops.ml | 25 +++++--------------------
 1 file changed, 5 insertions(+), 20 deletions(-)

(limited to 'engine')

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
-- 
cgit v1.2.3