diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 44 |
1 files changed, 27 insertions, 17 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3b8fb48eb0..4bc8d61258 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -478,7 +478,7 @@ let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite." let rec decompose_app_rel env evd t = (* Head normalize for compatibility with the old meta mechanism *) - let t = Reductionops.whd_betaiota evd t in + let t = Reductionops.whd_betaiota env evd t in match EConstr.kind evd t with | App (f, [||]) -> assert false | App (f, [|arg|]) -> @@ -711,7 +711,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs) ~fail:true env sigma in let evd = solve_remaining_by env sigma holes by in - let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in + let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta env evd c) in let c1 = nf c1 and c2 = nf c2 and rew_car = nf car and rel = nf rel and prf = nf prf in @@ -971,7 +971,7 @@ let unfold_match env sigma sk app = | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in - Reductionops.whd_beta sigma (mkApp (v, args)) + Reductionops.whd_beta env sigma (mkApp (v, args)) | _ -> app let is_rew_cast = function RewCast _ -> true | _ -> false @@ -1566,7 +1566,8 @@ let assert_replacing id newt tac = Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) let newfail n s = - Proofview.tclZERO (Refiner.FailError (n, lazy s)) + let info = Exninfo.reify () in + Proofview.tclZERO ~info (Refiner.FailError (n, lazy s)) let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in @@ -1576,8 +1577,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") - | Some None -> if progress then newfail 0 (str"Failed to progress") - else Proofview.tclUNIT () + | Some None -> + if progress + then newfail 0 (str"Failed to progress") + else Proofview.tclUNIT () | Some (Some res) -> let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in @@ -1641,7 +1644,9 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let tactic_init_setoid () = try init_setoid (); Proofview.tclUNIT () - with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded") + with e when CErrors.noncritical e -> + let _, info = Exninfo.capture e in + Tacticals.New.tclFAIL ~info 0 (str"Setoid library not loaded") let cl_rewrite_clause_strat progress strat clause = tactic_init_setoid () <*> @@ -1650,10 +1655,11 @@ let cl_rewrite_clause_strat progress strat clause = (cl_rewrite_clause_newtac ~progress strat clause) (fun (e, info) -> match e with | RewriteFailure e -> - tclZEROMSG (str"setoid rewrite failed: " ++ e) + tclZEROMSG ~info (str"setoid rewrite failed: " ++ e) | Refiner.FailError (n, pp) -> - tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) - | e -> Proofview.tclZERO ~info e)) + tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp) + | e -> + Proofview.tclZERO ~info e)) (** Setoid rewriting when called with "setoid_rewrite" *) let cl_rewrite_clause l left2right occs clause = @@ -2109,7 +2115,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals = (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) (fun (e, info) -> match e with | RewriteFailure e -> - tclFAIL 0 (str"setoid rewrite failed: " ++ e) + tclFAIL ~info 0 (str"setoid rewrite failed: " ++ e) | e -> Proofview.tclZERO ~info e) end @@ -2117,8 +2123,8 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite (** [setoid_]{reflexivity,symmetry,transitivity} tactics *) -let not_declared env sigma ty rel = - tclFAIL 0 +let not_declared ~info env sigma ty rel = + tclFAIL ~info 0 (str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++ str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library") @@ -2135,7 +2141,10 @@ let setoid_proof ty fn fallback = let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel - with e -> Proofview.tclZERO e + with e -> + (* XXX what is the right test here as to whether e can be converted ? *) + let e, info = Exninfo.capture e in + Proofview.tclZERO ~info e end begin function | e -> @@ -2145,9 +2154,10 @@ let setoid_proof ty fn fallback = | Hipattern.NoEquationFound -> begin match e with | (Not_found, _) -> - let rel, _, _ = decompose_app_rel env sigma concl in - not_declared env sigma ty rel - | (e, info) -> Proofview.tclZERO ~info e + let rel, _, _ = decompose_app_rel env sigma concl in + not_declared ~info env sigma ty rel + | (e, info) -> + Proofview.tclZERO ~info e end | e' -> Proofview.tclZERO ~info e' end |