diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 10 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 2 |
2 files changed, 8 insertions, 4 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 4306a9673..a0bffd4fb 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -32,7 +32,6 @@ open Evd let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e c = quote (pr_lconstr_env e c) -let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c) let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t) let pr_db env i = @@ -826,8 +825,12 @@ let error_ill_formed_constructor env id c v nparams nargs = else mt()) ++ str "." +let pr_ltype_using_barendregt_convention_env env c = + (* Use goal_concl_style as an approximation of Barendregt's convention (?) *) + quote (pr_goal_concl_style_env env c) + let error_bad_ind_parameters env c n v1 v2 = - let pc = pr_lconstr_env_at_top env c in + let pc = pr_ltype_using_barendregt_convention_env env c in let pv1 = pr_lconstr_env env v1 in let pv2 = pr_lconstr_env env v2 in str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ @@ -985,7 +988,8 @@ let explain_pattern_matching_error env = function let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,c,(env',e)) -> - str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++ + str "The abstracted term" ++ spc () ++ + quote (pr_goal_concl_style_env env c) ++ spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' Evd.empty e diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 4f365ebcf..7f01f0307 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -407,7 +407,7 @@ let process_goal sigma g = let env = Goal.V82.env sigma g in let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in + string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in let process_hyp h_env d acc = let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in (string_of_ppcmds (pr_var_decl h_env d)) :: acc in |