diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 2 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 2 | ||||
| -rw-r--r-- | plugins/fourier/fourierR.ml | 2 | ||||
| -rw-r--r-- | plugins/quote/quote.ml | 2 |
4 files changed, 4 insertions, 4 deletions
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 |