From 19a2dd5cfbd72defe932656a65ab9da9f4ac9d1e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 31 Oct 2016 20:25:28 +0100
Subject: 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.
---
 plugins/btauto/refl_btauto.ml | 2 +-
 plugins/cc/cctac.ml           | 2 +-
 plugins/fourier/fourierR.ml   | 2 +-
 plugins/quote/quote.ml        | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 6e8b2eb0fb..2c5b108e55 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 aedecc15c1..b5ca2f50fc 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 51bd3009ae..8e193c753e 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 b3ea4335f6..6405c8cebd 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
-- 
cgit v1.2.3