Moving unused code out of the kernel into Termops.

Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.

12 files changed, 30 insertions, 53 deletions

diff --git a/checker/term.mli b/checker/term.mli
index 0af83e05d..6b026d056 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -4,8 +4,6 @@ open Cic
 val family_of_sort : sorts -> sorts_family
 val family_equal : sorts_family -> sorts_family -> bool
 
-val strip_outer_cast : constr -> constr
-val collapse_appl : constr -> constr
 val decompose_app : constr -> constr * constr list
 val applist : constr * constr list -> constr
 val iter_constr_with_binders :
diff --git a/engine/termops.ml b/engine/termops.ml
index 04f55f2c3..35917b368 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -678,6 +678,21 @@ let rec subst_meta bl c =
     | Meta i -> (try Int.List.assoc i bl with Not_found -> c)
     | _ -> map_constr (subst_meta bl) c
 
+let rec strip_outer_cast c = match kind_of_term c with
+  | Cast (c,_,_) -> strip_outer_cast c
+  | _ -> c
+
+(* flattens application lists throwing casts in-between *)
+let collapse_appl c = match kind_of_term c with
+  | App (f,cl) ->
+      let rec collapse_rec f cl2 =
+        match kind_of_term (strip_outer_cast f) with
+        | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+        | _ -> mkApp (f,cl2)
+      in
+      collapse_rec f cl
+  | _ -> c
+
 (* First utilities for avoiding telescope computation for subst_term *)
 
 let prefix_application eq_fun (k,c) (t : constr) =
diff --git a/engine/termops.mli b/engine/termops.mli
index c58e3728c..78826f79a 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -164,6 +164,13 @@ val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*)
 
 val eta_reduce_head : constr -> constr
 
+(** Flattens application lists *)
+val collapse_appl : constr -> constr
+
+(** Remove recursively the casts around a term i.e.
+   [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
+val strip_outer_cast : constr -> constr
+
 exception CannotFilter
 
 (** Lightweight first-order filtering procedure. Unification
diff --git a/kernel/term.ml b/kernel/term.ml
index 08f888868..62c161be4 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -328,38 +328,9 @@ let destCoFix c = match kind_of_term c with
 let isCoFix c =  match kind_of_term c with CoFix _ -> true | _ -> false
 
 (******************************************************************)
-(* Cast management                                                *)
-(******************************************************************)
-
-let rec strip_outer_cast c = match kind_of_term c with
-  | Cast (c,_,_) -> strip_outer_cast c
-  | _ -> c
-
-(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *)
-
-let under_outer_cast f c =  match kind_of_term c with
-  | Cast (b,k,t) -> mkCast (f b, k, f t)
-  | _ -> f c
-
-let rec under_casts f c = match kind_of_term c with
-  | Cast (c,k,t) -> mkCast (under_casts f c, k, t)
-  | _            -> f c
-
-(******************************************************************)
 (* Flattening and unflattening of embedded applications and casts *)
 (******************************************************************)
 
-(* flattens application lists throwing casts in-between *)
-let collapse_appl c = match kind_of_term c with
-  | App (f,cl) ->
-      let rec collapse_rec f cl2 =
-        match kind_of_term (strip_outer_cast f) with
-        | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-        | _ -> mkApp (f,cl2)
-      in
-      collapse_rec f cl
-  | _ -> c
-
 let decompose_app c =
   match kind_of_term c with
     | App (f,cl) -> (f, Array.to_list cl)
diff --git a/kernel/term.mli b/kernel/term.mli
index 60a3c7715..a8d9dfbff 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -349,20 +349,6 @@ val strip_lam_n : int -> constr -> constr
 val strip_prod_assum : types -> types
 val strip_lam_assum : constr -> constr
 
-(** Flattens application lists *)
-val collapse_appl : constr -> constr
-
-
-(** Remove recursively the casts around a term i.e.
-   [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
-val strip_outer_cast : constr -> constr
-
-(** Apply a function letting Casted types in place *)
-val under_casts : (constr -> constr) -> constr -> constr
-
-(** Apply a function under components of Cast if any *)
-val under_outer_cast : (constr -> constr) -> constr -> constr
-
 (** {5 ... } *)
 (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
     Such a term can canonically be seen as the pair of a context of types
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 6e8b2eb0f..2c5b108e5 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -15,7 +15,7 @@ let get_inductive dir s =
   Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ()))
 
 let decomp_term (c : Term.constr) =
-  Term.kind_of_term (Term.strip_outer_cast c)
+  Term.kind_of_term (Termops.strip_outer_cast c)
 
 let lapp c v  = Term.mkApp (Lazy.force c, v)
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index aedecc15c..b5ca2f50f 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -86,7 +86,7 @@ let rec decompose_term env sigma t=
 	let p' = Projection.map canon_const p in
 	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->
-       let t = strip_outer_cast t in
+       let t = Termops.strip_outer_cast t in
        if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 51bd3009a..8e193c753 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -462,7 +462,7 @@ let rec fourier () =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
-    let goal = strip_outer_cast concl in
+    let goal = Termops.strip_outer_cast concl in
     let fhyp=Id.of_string "new_hyp_for_fourier" in
     (* si le but est une inéquation, on introduit son contraire,
        et le but à prouver devient False *)
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index b3ea4335f..6405c8ceb 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -183,7 +183,7 @@ type inversion_scheme = {
 
 let i_can't_do_that () = error "Quote: not a simple fixpoint"
 
-let decomp_term c = kind_of_term (strip_outer_cast c)
+let decomp_term c = kind_of_term (Termops.strip_outer_cast c)
 
 (*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ...
   ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index aa1a489c2..9ada04317 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -396,7 +396,7 @@ let subst_deps expand obls deps t =
     (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
 
 let rec prod_app t n =
-  match kind_of_term (strip_outer_cast t) with
+  match kind_of_term (Termops.strip_outer_cast t) with
     | Prod (_,_,b) -> subst1 n b
     | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
     | _ ->
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 46daacb58..d319b2419 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -112,7 +112,7 @@ let generic_search glnumopt fn =
 (** This function tries to see whether the conclusion matches a pattern. *)
 (** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
 let rec pattern_filter pat ref env typ =
-  let typ = strip_outer_cast typ in
+  let typ = Termops.strip_outer_cast typ in
   if Constr_matching.is_matching env Evd.empty pat typ then true
   else match kind_of_term typ with
   | Prod (_, _, typ)
@@ -120,7 +120,7 @@ let rec pattern_filter pat ref env typ =
   | _ -> false
 
 let rec head_filter pat ref env typ =
-  let typ = strip_outer_cast typ in
+  let typ = Termops.strip_outer_cast typ in
   if Constr_matching.is_matching_head env Evd.empty pat typ then true
   else match kind_of_term typ with
   | Prod (_, _, typ)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2c7fd46cf..ede88399e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -107,7 +107,7 @@ let show_intro all =
   let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
   if not (List.is_empty gls) then begin
     let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
-    let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
+    let l,_= decompose_prod_assum (Termops.strip_outer_cast (pf_concl gl)) in
     if all then
       let lid = Tactics.find_intro_names l gl in
       Feedback.msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))