From 118d24281bc62bb7ff503abee56f156545eb9eea Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 10 Mar 2018 23:54:14 +0100 Subject: [api] Remove deprecated object from `Term` We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it. --- tactics/btermdn.ml | 2 +- tactics/class_tactics.ml | 1 + tactics/contradiction.ml | 2 +- tactics/eauto.ml | 2 +- tactics/eqdecide.ml | 2 +- tactics/equality.ml | 1 + tactics/hints.ml | 2 +- tactics/hipattern.ml | 2 +- tactics/inv.ml | 1 + tactics/leminv.ml | 2 +- tactics/tacticals.ml | 2 +- tactics/tactics.ml | 4 ++-- tactics/term_dnet.ml | 2 +- 13 files changed, 14 insertions(+), 11 deletions(-) (limited to 'tactics') diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 8f50b0aa2..aca7f6c65 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -9,7 +9,7 @@ (************************************************************************) open Util -open Term +open Constr open EConstr open Names open Pattern diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3e08c6d87..28eaf9f28 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -18,6 +18,7 @@ open CErrors open Util open Names open Term +open Constr open Termops open EConstr open Tacmach diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c285f21e7..b92bc75bc 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Term +open Constr open EConstr open Hipattern open Tactics diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 3df9e3f82..80d07c5c0 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Termops open EConstr open Proof_type diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index b0deeed17..176701d99 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -17,7 +17,7 @@ open Util open Names open Namegen -open Term +open Constr open EConstr open Declarations open Tactics diff --git a/tactics/equality.ml b/tactics/equality.ml index 8904cd170..f9e06391a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -15,6 +15,7 @@ open Util open Names open Nameops open Term +open Constr open Termops open EConstr open Vars diff --git a/tactics/hints.ml b/tactics/hints.ml index 7b5be4c1c..7b943b373 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -12,7 +12,7 @@ open Pp open Util open CErrors open Names -open Term +open Constr open Evd open EConstr open Vars diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b8f1ed720..5d264058a 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Termops open EConstr open Inductiveops diff --git a/tactics/inv.ml b/tactics/inv.ml index b346ed223..28cfd57a2 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -14,6 +14,7 @@ open Util open Names open Term open Termops +open Constr open EConstr open Vars open Namegen diff --git a/tactics/leminv.ml b/tactics/leminv.ml index a4cdc1592..f47e6b2cd 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -12,9 +12,9 @@ open Pp open CErrors open Util open Names -open Term open Termops open Environ +open Constr open EConstr open Vars open Namegen diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 6c7db26c7..732d06f8a 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -509,7 +509,7 @@ module New = struct match Evd.evar_body evi with | Evd.Evar_empty -> Some (evk,evi) | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with - | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk + | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk | _ -> (* We make the assumption that there is no way to refine an evar remaining after typing from the initial term given to diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bb57e2bf4..58c62af85 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1910,8 +1910,8 @@ let cast_no_check cast c = exact_no_check (mkCast (c, cast, concl)) end -let vm_cast_no_check c = cast_no_check Term.VMcast c -let native_cast_no_check c = cast_no_check Term.NATIVEcast c +let vm_cast_no_check c = cast_no_check VMcast c +let native_cast_no_check c = cast_no_check NATIVEcast c let exact_proof c = let open Tacmach.New in diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 611799990..8bdcc6321 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -290,7 +290,7 @@ struct | Const (c,u) -> Term (DRef (ConstRef c)) | Ind (i,u) -> Term (DRef (IndRef i)) | Construct (c,u)-> Term (DRef (ConstructRef c)) - | Term.Meta _ -> assert false + | Meta _ -> assert false | Evar (i,_) -> let meta = try Evar.Map.find i !metas -- cgit v1.2.3