diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/certificate.ml | 5 | ||||
| -rw-r--r-- | plugins/micromega/zify.ml | 11 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 27 |
3 files changed, 27 insertions, 16 deletions
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/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 = |