aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/tacinterp.ml48
-rw-r--r--plugins/micromega/certificate.ml5
-rw-r--r--plugins/micromega/zify.ml11
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssrelim.ml27
5 files changed, 61 insertions, 32 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fdebe14a23..3228c6afd4 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -161,27 +161,45 @@ let catching_error call_trace fail (e, info) =
fail located_exc
end
-let update_loc ?loc (e, info) =
- (e, Option.cata (Loc.add_loc info) info loc)
+let update_loc loc use_finer (e, info as e') =
+ match loc with
+ | Some loc ->
+ if use_finer then
+ (* ensure loc if there is none *)
+ match Loc.get_loc info with
+ | None -> (e, Loc.add_loc info loc)
+ | _ -> (e, info)
+ else
+ (* override loc (because loc refers to inside of Ltac functions) *)
+ (e, Loc.add_loc info loc)
+ | None -> e'
-let catch_error ?loc call_trace f x =
+let catch_error_with_trace_loc loc use_finer call_trace f x =
try f x
with e when CErrors.noncritical e ->
let e = Exninfo.capture e in
- let e = update_loc ?loc e in
+ let e = update_loc loc use_finer e in
catching_error call_trace Exninfo.iraise e
-let catch_error_loc ?loc tac =
+let catch_error_loc loc use_finer tac =
Proofview.tclOR tac (fun exn ->
- let (e, info) = update_loc ?loc exn in
+ let (e, info) = update_loc loc use_finer exn in
Proofview.tclZERO ~info e)
-let wrap_error ?loc tac k =
+let wrap_error tac k =
+ if is_traced () then Proofview.tclORELSE tac k else tac
+
+let wrap_error_loc loc use_finer tac k =
if is_traced () then Proofview.tclORELSE tac k
- else catch_error_loc ?loc tac
+ else catch_error_loc loc use_finer tac
+
+let catch_error_tac call_trace tac =
+ wrap_error
+ tac
+ (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
-let catch_error_tac ?loc call_trace tac =
- wrap_error ?loc
+let catch_error_tac_loc loc use_finer call_trace tac =
+ wrap_error_loc loc use_finer
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -553,7 +571,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
let loc = loc_of_glob_constr term in
let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in
let (evd,c) =
- catch_error ?loc trace (understand_ltac flags env sigma vars kind) term
+ catch_error_with_trace_loc loc true trace (understand_ltac flags env sigma vars kind) term
in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
@@ -1071,7 +1089,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let call = LtacAtomCall t in
let trace = push_trace(loc,call) ist in
Profile_ltac.do_profile "eval_tactic:2" trace
- (catch_error_tac ?loc trace (interp_atomic ist t))
+ (catch_error_tac_loc loc true trace (interp_atomic ist t))
| TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
| TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
| TacId s ->
@@ -1162,7 +1180,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
; poly
; extra = TacStore.set ist.extra f_trace trace } in
val_interp ist alias.Tacenv.alias_body >>= fun v ->
- Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v))
+ Ftactic.lift (catch_error_loc loc false (tactic_of_value ist v))
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1191,7 +1209,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
- Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist))
+ Proofview.Trace.name_tactic name (catch_error_tac_loc loc false trace (tac args ist))
in
Ftactic.run args tac
@@ -1294,7 +1312,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
; extra = TacStore.set ist.extra f_trace []
} in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
- (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v ->
+ (catch_error_tac_loc loc false trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 9eeba614c7..148c1772bf 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -1020,10 +1020,11 @@ let lia (can_enum : bool) (prfdepth : int) sys =
p)
sys
end;
+ let bnd1 = bound_monomials sys in
let sys = subst sys in
- let bnd = bound_monomials sys in
+ let bnd2 = bound_monomials sys in
(* To deal with non-linear monomials *)
- let sys = bnd @ saturate_by_linear_equalities sys @ sys in
+ let sys = bnd1 @ bnd2 @ saturate_by_linear_equalities sys @ sys in
let sys' = List.map (fun ((p, o), prf) -> (cstr_of_poly (p, o), prf)) sys in
xlia (List.map fst sys) can_enum reduction_equations sys'
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 4e1f9a66ac..fa29e6080e 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -1324,9 +1324,14 @@ let do_let tac (h : Constr.named_declaration) =
let env = Tacmach.New.pf_env gl in
let evd = Tacmach.New.project gl in
try
- ignore (get_injection env evd (EConstr.of_constr ty));
- tac id.Context.binder_name (EConstr.of_constr t)
- (EConstr.of_constr ty)
+ let x = id.Context.binder_name in
+ ignore
+ (let eq = Lazy.force eq in
+ find_option
+ (match_operator env evd eq
+ [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|])
+ (HConstr.find_all eq !table_cache));
+ tac x (EConstr.of_constr t) (EConstr.of_constr ty)
with Not_found -> Tacticals.New.tclIDTAC)
let iter_let_aux tac =
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1b7768852e..d7996a722a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1352,7 +1352,7 @@ let unsafe_intro env decl b =
Refine.refine ~typecheck:false begin fun sigma ->
let ctx = Environ.named_context_val env in
let nctx = EConstr.push_named_context_val decl ctx in
- let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in
+ let inst = EConstr.identity_subst_val (Environ.named_context_val env) in
let ninst = EConstr.mkRel 1 :: inst in
let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 1c81fbc10b..1e182b52fa 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -485,17 +485,22 @@ let revtoptac n0 =
Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))
end
-let equality_inj l b id c =
- Proofview.V82.tactic begin fun gl ->
- let msg = ref "" in
- try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
- with
- | CErrors.UserError (_,s)
- when msg := Pp.string_of_ppcmds s;
- !msg = "Not a projectable equality but a discriminable one." ||
- !msg = "Nothing to inject." ->
- Feedback.msg_warning (Pp.str !msg);
- discharge_hyp (id, (id, "")) gl
+let nothing_to_inject =
+ CWarnings.create ~name:"spurious-ssr-injection" ~category:"ssr"
+ (fun (sigma, env, ty) ->
+ Pp.(str "SSReflect: cannot obtain new equations out of" ++ fnl() ++
+ str" " ++ Printer.pr_econstr_env env sigma ty ++ fnl() ++
+ str "Did you write an extra [] in the intro pattern?"))
+
+let equality_inj l b id c = Proofview.Goal.enter begin fun gl ->
+ Proofview.tclORELSE (Equality.inj None l b None c)
+ (function
+ | (Equality.NothingToInject,_) ->
+ let open Proofview.Notations in
+ Ssrcommon.tacTYPEOF (EConstr.mkVar id) >>= fun ty ->
+ nothing_to_inject (Proofview.Goal.sigma gl, Proofview.Goal.env gl, ty);
+ Proofview.V82.tactic (discharge_hyp (id, (id, "")))
+ | (e,info) -> Proofview.tclZERO ~info e)
end
let injectidl2rtac id c =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:14:04 +0000