diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 4 | ||||
| -rw-r--r-- | plugins/ltac/pltac.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/pltac.mli | 1 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 35 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 12 |
5 files changed, 31 insertions, 23 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 0b5d36b845..4a2c298caa 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -608,7 +608,7 @@ END { let subst_var_with_hole occ tid t = - let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in + let occref = if occ > 0 then ref occ else Locusops.error_invalid_occurrence [occ] in let locref = ref 0 in let rec substrec x = match DAst.get x with | GVar id -> @@ -628,7 +628,7 @@ let subst_var_with_hole occ tid t = | _ -> map_glob_constr_left_to_right substrec x in let t' = substrec t in - if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' + if !occref > 0 then Locusops.error_invalid_occurrence [occ] else t' let subst_hole_with_term occ tc t = let locref = ref 0 in diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 80c13a3698..196a68e67c 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -47,6 +47,8 @@ let binder_tactic = Entry.create "binder_tactic" let tactic = Entry.create "tactic" (* Main entry for quotations *) +let tactic_eoi = eoi_entry tactic + let () = let open Stdarg in let open Tacarg in diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 73bce84d18..c0bf6b9f76 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -40,3 +40,4 @@ val tactic_expr : raw_tactic_expr Entry.t [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"] val binder_tactic : raw_tactic_expr Entry.t val tactic : raw_tactic_expr Entry.t +val tactic_eoi : raw_tactic_expr Entry.t diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 77162ce89a..59533eb3e3 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -855,26 +855,20 @@ let coerce env cstr res = let res = { res with rew_evars = evars } in apply_constraint env res.rew_car rel prf cstr res -let apply_rule unify loccs : int pure_strategy = - let (nowhere_except_in,occs) = convert_occs loccs in - let is_occ occ = - if nowhere_except_in - then List.mem occ occs - else not (List.mem occ occs) - in - { strategy = fun { state = occ ; env ; +let apply_rule unify : occurrences_count pure_strategy = + { strategy = fun { state = occs ; env ; term1 = t ; ty1 = ty ; cstr ; evars } -> let unif = if isEvar (goalevars evars) t then None else unify env evars t in match unif with - | None -> (occ, Fail) + | None -> (occs, Fail) | Some rew -> - let occ = succ occ in - if not (is_occ occ) then (occ, Fail) - else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) + let b, occs = update_occurrence_counter occs in + if not b then (occs, Fail) + else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occs, Identity) else let res = { rew with rew_car = ty } in let res = Success (coerce env cstr res) in - (occ, res) + (occs, res) } let apply_lemma l2r flags oc by loccs : strategy = { strategy = @@ -890,9 +884,10 @@ let apply_lemma l2r flags oc by loccs : strategy = { strategy = | None -> None | Some rew -> Some rew in - let _, res = (apply_rule unify loccs).strategy { input with - state = 0 ; + let loccs, res = (apply_rule unify).strategy { input with + state = initialize_occurrence_counter loccs ; evars } in + check_used_occurrences loccs; (), res } @@ -1423,12 +1418,13 @@ let rewrite_with l2r flags c occs : strategy = { strategy = let (sigma, rew) = refresh_hypinfo env sigma c in unify_eqn rew l2r flags env (sigma, cstrs) None t in - let app = apply_rule unify occs in + let app = apply_rule unify in let strat = Strategies.fix (fun aux -> Strategies.choice app (subterm true default_flags aux)) in - let _, res = strat.strategy { input with state = 0 } in + let occs, res = strat.strategy { input with state = initialize_occurrence_counter occs } in + check_used_occurrences occs; ((), res) } @@ -2076,11 +2072,12 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals = Proofview.Goal.enter begin fun gl -> let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in let unify env evars t = unify_abs res l2r sort env evars t in - let app = apply_rule unify occs in + let app = apply_rule unify in let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in let substrat = Strategies.fix recstrat in let strat = { strategy = fun ({ state = () } as input) -> - let _, res = substrat.strategy { input with state = 0 } in + let occs, res = substrat.strategy { input with state = initialize_occurrence_counter occs } in + check_used_occurrences occs; (), res } in diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 4c1fe6417e..9abdc2ddbe 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -429,7 +429,15 @@ let pr_value env v = | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) -let error_ltac_variable ?loc id env v s = - CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++ +exception CoercionError of Id.t * (Environ.env * Evd.evar_map) option * Val.t * string + +let () = CErrors.register_handler begin function +| CoercionError (id, env, v, s) -> + Some (str "Ltac variable " ++ Id.print id ++ strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ strbrk "which cannot be coerced to " ++ str s ++ str".") +| _ -> None +end + +let error_ltac_variable ?loc id env v s = + Loc.raise ?loc (CoercionError (id, env, v, s)) |