aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_ltac.mlg1
-rw-r--r--plugins/ltac/profile_ltac.ml1
-rw-r--r--plugins/ltac/rewrite.ml29
-rw-r--r--plugins/ltac/taccoerce.ml4
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--plugins/ltac/tactic_debug.ml1
-rw-r--r--plugins/ltac/tauto.ml1
8 files changed, 19 insertions, 24 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 6c63a891e8..513f5ca77b 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -736,7 +736,7 @@ let refl_equal () = Coqlib.lib_ref "core.eq.type"
call it before it is defined. *)
let mkCaseEq a : unit Proofview.tactic =
Proofview.Goal.enter begin fun gl ->
- let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in
+ let type_of_a = Tacmach.New.pf_get_type_of gl a in
Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req ->
Tacticals.New.tclTHENLIST
[Tactics.generalize [(mkApp(req, [| type_of_a; a|]))];
@@ -794,7 +794,7 @@ let destauto t =
let destauto_in id =
Proofview.Goal.enter begin fun gl ->
- let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
+ let ctype = Tacmach.New.pf_get_type_of gl (mkVar id) in
(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
(* Pp.msgnl (Printer.pr_lconstr (ctype)); *)
destauto ctype
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 81a6651745..7ea843ca69 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -368,7 +368,6 @@ let print_info_trace = ref None
let () = declare_int_option {
optdepr = false;
- optname = "print info trace";
optkey = ["Info" ; "Level"];
optread = (fun () -> !print_info_trace);
optwrite = fun n -> print_info_trace := n;
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index fe5ebf1172..7529f9fce6 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -450,7 +450,6 @@ let () =
let open Goptions in
declare_bool_option
{ optdepr = false;
- optname = "Ltac Profiling";
optkey = ["Ltac"; "Profiling"];
optread = get_profiling;
optwrite = set_profiling }
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 98d14f3d33..fbc64d95d0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -289,18 +289,18 @@ end) = struct
if Int.equal n 0 then c
else
match EConstr.kind sigma c with
- | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
+ | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f ->
decomp_pointwise sigma (pred n) relb
- | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
+ | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f ->
decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1]))
| _ -> invalid_arg "decomp_pointwise"
let rec apply_pointwise sigma rel = function
| arg :: args ->
(match EConstr.kind sigma rel with
- | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
+ | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f ->
apply_pointwise sigma relb args
- | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
+ | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f ->
apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args
| _ -> invalid_arg "apply_pointwise")
| [] -> rel
@@ -357,7 +357,7 @@ end) = struct
match EConstr.kind sigma t with
| App (c, args) when Array.length args >= 2 ->
let head = if isApp sigma c then fst (destApp sigma c) else c in
- if Termops.is_global sigma (coq_eq_ref ()) head then None
+ if isRefX sigma (coq_eq_ref ()) head then None
else
(try
let params, args = Array.chop (Array.length args - 2) args in
@@ -483,7 +483,7 @@ let rec decompose_app_rel env evd t =
| App (f, [||]) -> assert false
| App (f, [|arg|]) ->
let (f', argl, argr) = decompose_app_rel env evd arg in
- let ty = Typing.unsafe_type_of env evd argl in
+ let ty = Retyping.get_type_of env evd argl in
let r = Retyping.relevance_of_type env evd ty in
let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty,
mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty,
@@ -789,7 +789,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let morphargs, morphobjs = Array.chop first args in
let morphargs', morphobjs' = Array.chop first args' in
let appm = mkApp(m, morphargs) in
- let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
+ let evd, appmtype = Typing.type_of env (goalevars evars) appm in
+ let evars = evd, snd evars in
let cstrs = List.map
(Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
(Array.to_list morphobjs')
@@ -1879,13 +1880,13 @@ let declare_projection n instance_id r =
let rec aux t =
match EConstr.kind sigma t with
| App (f, [| a ; a' ; rel; rel' |])
- when Termops.is_global sigma (PropGlobal.respectful_ref ()) f ->
+ when isRefX sigma (PropGlobal.respectful_ref ()) f ->
succ (aux rel')
| _ -> 0
in
let init =
match EConstr.kind sigma typ with
- App (f, args) when Termops.is_global sigma (PropGlobal.respectful_ref ()) f ->
+ App (f, args) when isRefX sigma (PropGlobal.respectful_ref ()) f ->
mkApp (f, fst (Array.chop (Array.length args - 2) args))
| _ -> typ
in aux init
@@ -1906,7 +1907,7 @@ let declare_projection n instance_id r =
let build_morphism_signature env sigma m =
let m,ctx = Constrintern.interp_constr env sigma m in
let sigma = Evd.from_ctx ctx in
- let t = Typing.unsafe_type_of env sigma m in
+ let t = Retyping.get_type_of env sigma m in
let cstrs =
let rec aux t =
match EConstr.kind sigma t with
@@ -1936,7 +1937,7 @@ let build_morphism_signature env sigma m =
let default_morphism sign m =
let env = Global.env () in
let sigma = Evd.from_env env in
- let t = Typing.unsafe_type_of env sigma m in
+ let t = Retyping.get_type_of env sigma m in
let evars, _, sign, cstrs =
PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
in
@@ -2195,10 +2196,10 @@ let setoid_transitivity c =
(transitivity_red true c)
let setoid_symmetry_in id =
- let open Tacmach.New in
Proofview.Goal.enter begin fun gl ->
- let sigma = project gl in
- let ctype = pf_unsafe_type_of gl (mkVar id) in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let ctype = Retyping.get_type_of env sigma (mkVar id) in
let binders,concl = decompose_prod_assum sigma ctype in
let (equiv, args) = decompose_app sigma concl in
let rec split_last_two = function
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index a57cc76faa..de70fb292a 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -341,8 +341,8 @@ let coerce_to_reference sigma v =
match Value.to_constr v with
| Some c ->
begin
- try fst (Termops.global_of_constr sigma c)
- with Not_found -> raise (CannotCoerceTo "a reference")
+ try fst (EConstr.destRef sigma c)
+ with DestKO -> raise (CannotCoerceTo "a reference")
end
| None -> raise (CannotCoerceTo "a reference")
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 98aa649b62..6e620b71db 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2082,7 +2082,6 @@ let () =
let open Goptions in
declare_bool_option
{ optdepr = false;
- optname = "Ltac debug";
optkey = ["Ltac";"Debug"];
optread = (fun () -> get_debug () != Tactic_debug.DebugOff);
optwrite = vernac_debug }
@@ -2091,7 +2090,6 @@ let () =
let open Goptions in
declare_bool_option
{ optdepr = false;
- optname = "Ltac Backtrace";
optkey = ["Ltac"; "Backtrace"];
optread = (fun () -> !log_trace);
optwrite = (fun b -> log_trace := b) }
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 539536911c..0e9465839a 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -86,7 +86,6 @@ open Goptions
let () =
declare_bool_option
{ optdepr = false;
- optname = "Ltac batch debug";
optkey = ["Ltac";"Batch";"Debug"];
optread = (fun () -> !batch);
optwrite = (fun x -> batch := x) }
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index ba759441e5..92110d7a43 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -68,7 +68,6 @@ open Goptions
let () =
declare_bool_option
{ optdepr = false;
- optname = "unfolding of not in intuition";
optkey = ["Intuition";"Negation";"Unfolding"];
optread = (fun () -> !negation_unfolding);
optwrite = (:=) negation_unfolding }
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 16:03:49 +0000