aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-06 23:27:09 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-06 23:46:52 +0100
commit03e21974a3e971a294533bffb81877dc1bd270b6 (patch)
tree1b37339378f6bc93288b61f707efb6b08f992dc5 /plugins/ltac
parentf3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff)
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml46
-rw-r--r--plugins/ltac/g_class.ml42
-rw-r--r--plugins/ltac/pptactic.ml8
-rw-r--r--plugins/ltac/rewrite.ml8
-rw-r--r--plugins/ltac/rewrite.mli2
-rw-r--r--plugins/ltac/taccoerce.ml6
6 files changed, 16 insertions, 16 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 65c186a41..4b1555e55 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -415,7 +415,7 @@ VERNAC COMMAND EXTEND DeriveInversionClear
-> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ]
+ -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ]
END
VERNAC COMMAND EXTEND DeriveInversion
@@ -424,7 +424,7 @@ VERNAC COMMAND EXTEND DeriveInversion
-> [ add_inversion_lemma_exn na c s false inv_tac ]
| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c InProp false inv_tac ]
+ -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ]
END
VERNAC COMMAND EXTEND DeriveDependentInversion
@@ -514,7 +514,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
-let inTransitivity : bool * Term.constr -> obj =
+let inTransitivity : bool * Constr.t -> obj =
declare_object {(default_object "TRANSITIVITY-STEPS") with
cache_function = cache_transitivity_lemma;
open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o);
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 104977aef..ed2d9da63 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -91,7 +91,7 @@ END
(** TODO: DEPRECATE *)
(* A progress test that allows to see if the evars have changed *)
-open Term
+open Constr
open Proofview.Notations
let rec eq_constr_mod_evars sigma x y =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e467d3e2c..6522fc28f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1120,10 +1120,10 @@ let pr_goal_selector ~toplevel s =
let ty = EConstr.Unsafe.to_constr ty in
let rec strip_ty acc n ty =
if n=0 then (List.rev acc, EConstr.of_constr ty) else
- match Term.kind_of_term ty with
- Term.Prod(na,a,b) ->
- strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
- | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
+ match Constr.kind ty with
+ | Constr.Prod(na,a,b) ->
+ strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_atomic_tactic_level env sigma n t =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1809f0fcd..705a51edd 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -12,7 +12,7 @@ open CErrors
open Util
open Nameops
open Namegen
-open Term
+open Constr
open EConstr
open Vars
open Reduction
@@ -426,7 +426,7 @@ let split_head = function
| [] -> assert(false)
let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
- pb == pb' || (ty == ty' && Term.eq_constr x x' && Term.eq_constr y y')
+ pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
let problem_inclusion x y =
List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
@@ -928,8 +928,8 @@ let fold_match ?(force=false) env sigma c =
it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
in
let sk =
- if sortp == InProp then
- if sortc == InProp then
+ if sortp == Sorts.InProp then
+ if sortc == Sorts.InProp then
if dep then case_dep_scheme_kind_from_prop
else case_scheme_kind_from_prop
else (
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 63e891b45..1306c590b 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -37,7 +37,7 @@ type ('constr,'redexpr) strategy_ast =
type rewrite_proof =
| RewPrf of constr * constr
- | RewCast of Term.cast_kind
+ | RewCast of Constr.cast_kind
type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4d171ecbc..c03a86732 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -8,7 +8,7 @@
open Util
open Names
-open Term
+open Constr
open EConstr
open Misctypes
open Genarg
@@ -172,8 +172,8 @@ let id_of_name = function
| Sort s ->
begin
match ESorts.kind sigma s with
- | Prop _ -> Label.to_id (Label.make "Prop")
- | Type _ -> Label.to_id (Label.make "Type")
+ | Sorts.Prop _ -> Label.to_id (Label.make "Prop")
+ | Sorts.Type _ -> Label.to_id (Label.make "Type")
end
| _ -> fail()