aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/Ltac.v0
-rw-r--r--plugins/ltac/evar_tactics.ml12
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_ltac.mlg1
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/profile_ltac.ml1
-rw-r--r--plugins/ltac/rewrite.ml43
-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
11 files changed, 34 insertions, 37 deletions
diff --git a/plugins/ltac/Ltac.v b/plugins/ltac/Ltac.v
deleted file mode 100644
index e69de29bb2..0000000000
--- a/plugins/ltac/Ltac.v
+++ /dev/null
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index c87eb7c3c9..3ea4974a87 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -26,9 +26,9 @@ module NamedDecl = Context.Named.Declaration
(* The instantiate tactic *)
-let instantiate_evar evk (ist,rawc) sigma =
+let instantiate_evar evk (ist,rawc) env sigma =
let evi = Evd.find sigma evk in
- let filtered = Evd.evar_filtered_env evi in
+ let filtered = Evd.evar_filtered_env env evi in
let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
let lvar = {
ltac_constrs = constrvars;
@@ -36,7 +36,7 @@ let instantiate_evar evk (ist,rawc) sigma =
ltac_idents = Names.Id.Map.empty;
ltac_genargs = ist.Geninterp.lfun;
} in
- let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in
+ let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in
tclEVARS sigma'
let evar_list sigma c =
@@ -48,6 +48,7 @@ let evar_list sigma c =
let instantiate_tac n c ido =
Proofview.V82.tactic begin fun gl ->
+ let env = Global.env () in
let sigma = gl.sigma in
let evl =
match ido with
@@ -69,16 +70,17 @@ let instantiate_tac n c ido =
user_err Pp.(str "Not enough uninstantiated existential variables.");
if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let evk,_ = List.nth evl (n-1) in
- instantiate_evar evk c sigma gl
+ instantiate_evar evk c env sigma gl
end
let instantiate_tac_by_name id c =
Proofview.V82.tactic begin fun gl ->
+ let env = Global.env () in
let sigma = gl.sigma in
let evk =
try Evd.evar_key id sigma
with Not_found -> user_err Pp.(str "Unknown existential variable.") in
- instantiate_evar evk c sigma gl
+ instantiate_evar evk c env sigma gl
end
let let_evar name typ =
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/pptactic.ml b/plugins/ltac/pptactic.ml
index 0e8c225a8f..7843faaef3 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -971,7 +971,7 @@ let pr_goal_selector ~toplevel s =
| TacTime (s,t) ->
hov 1 (
keyword "time"
- ++ pr_opt str s ++ spc ()
+ ++ pr_opt qstring s ++ spc ()
++ pr_tac (ltactical,E) t),
ltactical
| TacRepeat t ->
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 2998e1c767..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')
@@ -924,10 +925,10 @@ let reset_env env =
let env' = Global.env_of_context (Environ.named_context_val env) in
Environ.push_rel_context (Environ.rel_context env) env'
-let fold_match ?(force=false) env sigma c =
+let fold_match env sigma c =
let (ci, p, c, brs) = destCase sigma c in
let cty = Retyping.get_type_of env sigma c in
- let dep, pred, exists, (sk,eff) =
+ let dep, pred, exists, sk =
let env', ctx, body =
let ctx, pred = decompose_lam_assum sigma p in
let env' = push_rel_context ctx env in
@@ -954,8 +955,8 @@ let fold_match ?(force=false) env sigma c =
else case_scheme_kind_from_type)
in
let exists = Ind_tables.check_scheme sk ci.ci_ind in
- if exists || force then
- dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind
+ if exists then
+ dep, pred, exists, Ind_tables.lookup_scheme sk ci.ci_ind
else raise Not_found
in
let app =
@@ -964,7 +965,7 @@ let fold_match ?(force=false) env sigma c =
let meths = List.map (fun br -> br) (Array.to_list brs) in
applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
in
- sk, (if exists then env else reset_env env), app, eff
+ sk, (if exists then env else reset_env env), app
let unfold_match env sigma sk app =
match EConstr.kind sigma app with
@@ -1222,7 +1223,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
else
match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
| None -> state, c'
- | Some (cst, _, t', eff (*FIXME*)) ->
+ | Some (cst, _, t') ->
let state, res = aux { state ; env ; unfresh ;
term1 = t' ; ty1 = ty ;
cstr = (prop,cstr) ; evars } in
@@ -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
@@ -1930,13 +1931,13 @@ let build_morphism_signature env sigma m =
let evd = solve_constraints env !evd in
let evd = Evd.minimize_universes evd in
let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
- Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m);
+ Pretyping.check_evars env evd (EConstr.of_constr m);
Evd.evar_universe_context evd, 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-05-03 01:49:42 +0000