CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Context.{Rel,Named}.fold_constr"

10 files changed, 26 insertions, 16 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index fcee79e07..7b0ba1700 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,13 @@
 =========================================
+= CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
+=========================================
+
+We renamed the following functions:
+
+  Context.Rel.Declaration.fold   -> Context.Rel.Declaration.fold_constr
+  Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr
+
+=========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fcb429aef..326cd25fc 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -689,7 +689,7 @@ let undefined_evars_of_term evd t =
 
 let undefined_evars_of_named_context evd nc =
   Context.Named.fold_outside
-    (NamedDecl.fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
+    (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
     nc
     ~init:Evar.Set.empty
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 036abbdeb..d573a9f05 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -287,7 +287,7 @@ let metavars_of c =
   let rec collrec acc c =
     match kind_of_term c with
       | Meta mv -> Int.Set.add mv acc
-      | _         -> fold_constr collrec acc c
+      | _         -> Term.fold_constr collrec acc c
   in
   collrec Int.Set.empty c
 
@@ -734,20 +734,20 @@ let evar_list c =
   let rec evrec acc c =
     match kind_of_term c with
     | Evar (evk, _ as ev) -> ev :: acc
-    | _ -> fold_constr evrec acc c in
+    | _ -> Term.fold_constr evrec acc c in
   evrec [] c
 
 let evars_of_term c =
   let rec evrec acc c =
     match kind_of_term c with
     | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
-    | _ -> fold_constr evrec acc c
+    | _ -> Term.fold_constr evrec acc c
   in
   evrec Evar.Set.empty c
 
 let evars_of_named_context nc =
   Context.Named.fold_outside
-    (NamedDecl.fold (fun constr s -> Evar.Set.union s (evars_of_term constr)))
+    (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr)))
     nc
     ~init:Evar.Set.empty
 
diff --git a/kernel/context.ml b/kernel/context.ml
index 43be9fc4f..4c88283ca 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -138,7 +138,7 @@ struct
       | LocalDef (_,v,ty) -> f v; f ty
 
     (** Reduce all terms in a given declaration to a single value. *)
-    let fold f decl acc =
+    let fold_constr f decl acc =
       match decl with
       | LocalAssum (n,ty) -> f ty acc
       | LocalDef (n,v,ty) -> f ty (f v acc)
@@ -333,7 +333,7 @@ struct
       | LocalDef (_, v, ty) -> f v; f ty
 
     (** Reduce all terms in a given declaration to a single value. *)
-    let fold f decl a =
+    let fold_constr f decl a =
       match decl with
       | LocalAssum (_, ty) -> f ty a
       | LocalDef (_, v, ty) -> a |> f v |> f ty
diff --git a/kernel/context.mli b/kernel/context.mli
index 7c652ac5c..8ed09794b 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -79,7 +79,7 @@ sig
     val iter_constr : (Constr.t -> unit) -> t -> unit
 
     (** Reduce all terms in a given declaration to a single value. *)
-    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+    val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
 
     val to_tuple : t -> Name.t * Constr.t option * Constr.t
   end
@@ -192,7 +192,7 @@ sig
     val iter_constr : (Constr.t -> unit) -> t -> unit
 
     (** Reduce all terms in a given declaration to a single value. *)
-    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+    val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
 
     val to_tuple : t -> Id.t * Constr.t option * Constr.t
     val of_tuple : Id.t * Constr.t option * Constr.t -> t
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7351a87d4..8a147a659 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -416,7 +416,7 @@ let global_vars_set env constr =
 	  Id.Set.union (vars_of_global env c) acc
       | _ ->
 	  acc in
-    fold_constr filtrec acc c
+    Term.fold_constr filtrec acc c
   in
     filtrec Id.Set.empty constr
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index e59a17d12..8db65e33c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -22,6 +22,7 @@ open Entries
 open Typeops
 open Fast_typeops
 
+module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 let constrain_type env j poly subst = function
@@ -251,7 +252,7 @@ let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
   | TemplateArity (ctx,_) ->
       Context.Rel.fold_outside
-        (Context.Rel.Declaration.fold
+        (RelDecl.fold_constr
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 62f307115..65f96c831 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -377,7 +377,7 @@ type journey_info =
 let rec add_vars forbidden e = 
   match kind_of_term e with 
     | Var x -> x::forbidden 
-    | _ -> fold_constr add_vars forbidden e 
+    | _ -> Term.fold_constr add_vars forbidden e
 
 
 let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 19f5f5d3f..e12fe5d70 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -297,9 +297,9 @@ let collect_meta_variables c =
   let rec collrec deep acc c = match kind_of_term c with
     | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
     | Cast(c,_,_) -> collrec deep acc c
-    | (App _| Case _) -> fold_constr (collrec deep) acc c
+    | (App _| Case _) -> Term.fold_constr (collrec deep) acc c
     | Proj (_, c) -> collrec deep acc c
-    | _ -> fold_constr (collrec true) acc c
+    | _ -> Term.fold_constr (collrec true) acc c
   in
   List.rev (collrec false [] c)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d8c241193..7ee45523f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3470,8 +3470,8 @@ let ids_of_constr ?(all=false) vars c =
 	      Array.fold_left_from
 		(if all then 0 else mib.Declarations.mind_nparams)
 		aux vars args
-	| _ -> fold_constr aux vars c)
-    | _ -> fold_constr aux vars c
+	| _ -> Term.fold_constr aux vars c)
+    | _ -> Term.fold_constr aux vars c
   in aux vars c
 
 let decompose_indapp f args =