aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/tacinterp.ml')
-rw-r--r--ltac/tacinterp.ml58
1 files changed, 24 insertions, 34 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 08e67a0c2..92a403c58 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -31,7 +31,7 @@ open Tacexpr
open Genarg
open Geninterp
open Stdarg
-open Constrarg
+open Tacarg
open Printer
open Pretyping
open Misctypes
@@ -168,7 +168,7 @@ module Value = struct
let pr_v = Pptactic.pr_value Pptactic.ltop v in
let Val.Dyn (tag, _) = v in
let tag = Val.pr tag in
- errorlabstrm "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
+ user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
++ str " while type " ++ Val.pr wit ++ str " was expected.")
let unbox wit v ans = match ans with
@@ -315,8 +315,8 @@ let append_trace trace v =
(* Dynamically check that an argument is a tactic *)
let coerce_to_tactic loc id v =
let v = Value.normalize v in
- let fail () = user_err_loc
- (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
+ let fail () = user_err ~loc
+ (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
in
let v = Value.normalize v in
if has_type v (topwit wit_tacvalue) then
@@ -371,7 +371,7 @@ let debugging_exception_step ist signal_anomaly e pp =
pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
let error_ltac_variable loc id env v s =
- user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++
+ user_err ~loc (str "Ltac variable " ++ pr_id id ++
strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
strbrk "which cannot be coerced to " ++ str s ++ str".")
@@ -388,8 +388,6 @@ let interp_ident ist env sigma id =
try try_interp_ltac_var (coerce_var_to_ident false env) ist (Some (env,sigma)) (dloc,id)
with Not_found -> id
-let pf_interp_ident id gl = interp_ident id (pf_env gl) (project gl)
-
(* Interprets an optional identifier, bound or fresh *)
let interp_name ist env sigma = function
| Anonymous -> Anonymous
@@ -406,8 +404,8 @@ let interp_intro_pattern_naming_var loc ist env sigma id =
let interp_int ist locid =
try try_interp_ltac_var coerce_to_int ist None locid
with Not_found ->
- user_err_loc(fst locid,"interp_int",
- str "Unbound variable " ++ pr_id (snd locid) ++ str".")
+ user_err ~loc:(fst locid) ~hdr:"interp_int"
+ (str "Unbound variable " ++ pr_id (snd locid) ++ str".")
let interp_int_or_var ist = function
| ArgVar locid -> interp_int ist locid
@@ -429,7 +427,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
with Not_found ->
(* Then look if bound in the proof context at calling time *)
if is_variable env id then id
- else Loc.raise loc (Logic.RefinerError (Logic.NoSuchHyp id))
+ else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id))
let interp_hyp_list_as_list ist env sigma (loc,id as x) =
try coerce_to_hyp_list env (Id.Map.find id ist.lfun)
@@ -451,7 +449,7 @@ let interp_reference ist env sigma = function
with Not_found ->
try
VarRef (get_id (Environ.lookup_named id env))
- with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
+ with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
let try_interp_evaluable env (loc, id) =
let v = Environ.lookup_named id env in
@@ -467,14 +465,14 @@ let interp_evaluable ist env sigma = function
with Not_found ->
match r with
| EvalConstRef _ -> r
- | _ -> error_global_not_found_loc loc (qualid_of_ident id)
+ | _ -> error_global_not_found ~loc (qualid_of_ident id)
end
| ArgArg (r,None) -> r
| ArgVar (loc, id) ->
try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some (env,sigma)) (loc, id)
with Not_found ->
try try_interp_evaluable env (loc, id)
- with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
+ with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
(* Interprets an hypothesis name *)
let interp_occurrences ist occs =
@@ -696,9 +694,6 @@ let interp_typed_pattern ist env sigma (_,c,_) =
pattern_of_constr env sigma c
(* Interprets a constr expression *)
-let pf_interp_constr ist gl =
- interp_constr ist (pf_env gl) (project gl)
-
let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
let try_expand_ltac_var sigma x =
try match dest_fun x with
@@ -720,10 +715,6 @@ let interp_constr_list ist env sigma c =
let interp_open_constr_list =
interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_open_constr
-(* Interprets a type expression *)
-let pf_interp_type ist env sigma =
- interp_type ist env sigma
-
(* Interprets a reduction expression *)
let interp_unfold ist env sigma (occs,qid) =
(interp_occurrences ist occs,interp_evaluable ist env sigma qid)
@@ -748,7 +739,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
Inr (pattern_of_constr env sigma c) in
(try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
with Not_found ->
- error_global_not_found_loc loc (qualid_of_ident id))
+ error_global_not_found ~loc (qualid_of_ident id))
| Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
| Inr c -> Inr (interp_typed_pattern ist env sigma c) in
interp_occurrences ist occs, p
@@ -804,8 +795,8 @@ let interp_may_eval f ist env sigma = function
!evdref , c
with
| Not_found ->
- user_err_loc (loc, "interp_may_eval",
- str "Unbound context identifier" ++ pr_id s ++ str"."))
+ user_err ~loc ~hdr:"interp_may_eval"
+ (str "Unbound context identifier" ++ pr_id s ++ str"."))
| ConstrTypeOf c ->
let (sigma,c_interp) = f ist env sigma c in
Typing.type_of ~refresh:true env sigma c_interp
@@ -1041,8 +1032,8 @@ let interp_destruction_arg ist gl arg =
}
| keep,ElimOnAnonHyp n as x -> x
| keep,ElimOnIdent (loc,id) ->
- let error () = user_err_loc (loc, "",
- strbrk "Cannot coerce " ++ pr_id id ++
+ let error () = user_err ~loc
+ (strbrk "Cannot coerce " ++ pr_id id ++
strbrk " neither to a quantified hypothesis nor to a term.")
in
let try_cast_id id' =
@@ -1052,7 +1043,7 @@ let interp_destruction_arg ist gl arg =
(keep, ElimOnConstr { delayed = begin fun env sigma ->
try Sigma.here (constr_of_id env id', NoBindings) sigma
with Not_found ->
- user_err_loc (loc, "interp_destruction_arg",
+ user_err ~loc ~hdr:"interp_destruction_arg" (
pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
end })
in
@@ -1120,7 +1111,7 @@ let read_pattern lfun ist env sigma = function
(* Reads the hypotheses of a Match Context rule *)
let cons_and_check_name id l =
if Id.List.mem id l then
- user_err_loc (dloc,"read_match_goal_hyps",
+ user_err ~hdr:"read_match_goal_hyps" (
str "Hypothesis pattern-matching variable " ++ pr_id id ++
str " used twice in the same pattern.")
else id::l
@@ -1220,7 +1211,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
end
| TacAbstract (tac,ido) ->
Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT
- (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac)
+ (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
end }
| TacThen (t1,t) ->
Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
@@ -1706,7 +1697,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let env = pf_env gl in
let f sigma (id,n,c) =
- let (sigma,c_interp) = pf_interp_type ist env sigma c in
+ let (sigma,c_interp) = interp_type ist env sigma c in
sigma , (interp_ident ist env sigma id,n,c_interp) in
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
@@ -1721,7 +1712,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let env = pf_env gl in
let f sigma (id,c) =
- let (sigma,c_interp) = pf_interp_type ist env sigma c in
+ let (sigma,c_interp) = interp_type ist env sigma c in
sigma , (interp_ident ist env sigma id,c_interp) in
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
@@ -1763,7 +1754,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in
if Locusops.is_nowhere clp then
(* We try to fully-typecheck the term *)
- let (sigma,c_interp) = pf_interp_constr ist gl c in
+ let (sigma,c_interp) = interp_constr ist env sigma c in
let let_tac b na c cl eqpat =
let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
@@ -1876,7 +1867,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let (sigma, c) = interp_constr ist env sigma c in
Sigma.Unsafe.of_pair (c, sigma)
with e when to_catch e (* Hack *) ->
- errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+ user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
end } in
Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
end }
@@ -1911,7 +1902,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
match c with
| None -> sigma , None
| Some c ->
- let (sigma,c_interp) = pf_interp_constr ist gl c in
+ let (sigma,c_interp) = interp_constr ist env sigma c in
sigma , Some c_interp
in
let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
@@ -1978,7 +1969,6 @@ let interp_tac_gen lfun avoid_ids debug t =
end }
let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
-let _ = Proof_global.set_interp_tac interp
(* Used to hide interpretation for pretty-print, now just launch tactics *)
(* [global] means that [t] should be internalized outside of goals. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 17:32:00 +0000