diff options
author | 2014-09-04 12:10:08 +0200 | |
---|---|---|
committer | 2014-09-04 12:57:33 +0200 | |
commit | 6b0c471723a657048e50c94ea56387d54ef6eff6 (patch) | |
tree | 5bf4c2d87b611a77e29483b53ae9c5773ccb3bc1 | |
parent | a8a0cd9d5cf849be3b995ffc19e2cb4a0ff33d7a (diff) |
Revert "Tacinterp: [interp_message] and associate now only require an environment rather than an entire goal."
This reverts commit 4eaafcd00992302c186b8d11e890616726ebd822.
-rw-r--r-- | tactics/tacinterp.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cc1dcb453..f241b6373 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -710,14 +710,14 @@ let interp_constr_may_eval ist env sigma c = end (** TODO: should use dedicated printers *) -let rec message_of_value env v = +let rec message_of_value gl v = let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then str "<tactic>" else if has_type v (topwit wit_constr) then - pr_constr_env env (out_gen (topwit wit_constr) v) + pr_constr_env (pf_env gl) (out_gen (topwit wit_constr) v) else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in - pr_constr_under_binders_env env c + pr_constr_under_binders_env (pf_env gl) c else if has_type v (topwit wit_unit) then str "()" else if has_type v (topwit wit_int) then int (out_gen (topwit wit_int) v) else if has_type v (topwit wit_intro_pattern) then @@ -725,22 +725,22 @@ let rec message_of_value env v = (fun c -> pr_constr_env env (snd (c env Evd.empty))) (out_gen (topwit wit_intro_pattern) v) else if has_type v (topwit wit_constr_context) then - pr_constr_env env (out_gen (topwit wit_constr_context) v) + pr_constr_env (pf_env gl) (out_gen (topwit wit_constr_context) v) else match Value.to_list v with | Some l -> - let print v = message_of_value env v in + let print v = message_of_value gl v in prlist_with_sep spc print l | None -> str "<abstr>" (** TODO *) -let interp_message_token ist env = function +let interp_message_token ist gl = function | MsgString s -> str s | MsgInt n -> int n | MsgIdent (loc,id) -> let v = try Id.Map.find id ist.lfun with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found.") in - message_of_value env v + message_of_value gl v let interp_message_nl ist gl = function | [] -> mt() @@ -1103,12 +1103,12 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacId s -> Proofview.tclTHEN (Proofview.V82.tactic begin fun gl -> - tclIDTAC_MESSAGE (interp_message_nl ist (pf_env gl) s) gl + tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl end) (Proofview.tclLIFT (db_breakpoint (curr_debug ist) s)) | TacFail (n,s) -> Proofview.V82.tactic begin fun gl -> - tclFAIL (interp_int_or_var ist n) (interp_message ist (pf_env gl) s) gl + tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl end | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) | TacShowHyps tac -> |