diff options
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 37 |
1 files changed, 22 insertions, 15 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 0b9ce918..5352e0b7 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -35,13 +35,19 @@ let delayed_emacs_cmd s = (**********************************************************************) (** Terms *) - (* [at_top] means ids of env must be avoided in bound variables *) -let pr_constr_core at_top env t = - pr_constr_expr (extern_constr at_top env t) -let pr_lconstr_core at_top env t = - pr_lconstr_expr (extern_constr at_top env t) +(* [goal_concl_style] means that all names of goal/section variables + and all names of rel variables (if any) in the given env and all short + names of global definitions of the current module must be avoided while + printing bound variables. + Otherwise, short names of global definitions are printed qualified + and only names of goal/section variables and rel names that do + _not_ occur in the scope of the binder to be printed are avoided. *) + +let pr_constr_core goal_concl_style env t = + pr_constr_expr (extern_constr goal_concl_style env t) +let pr_lconstr_core goal_concl_style env t = + pr_lconstr_expr (extern_constr goal_concl_style env t) -let pr_lconstr_env_at_top env = pr_lconstr_core true env let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env @@ -68,12 +74,12 @@ let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_en let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c -let pr_type_core at_top env t = - pr_constr_expr (extern_type at_top env t) -let pr_ltype_core at_top env t = - pr_lconstr_expr (extern_type at_top env t) +let pr_type_core goal_concl_style env t = + pr_constr_expr (extern_type goal_concl_style env t) +let pr_ltype_core goal_concl_style env t = + pr_lconstr_expr (extern_type goal_concl_style env t) -let pr_ltype_env_at_top env = pr_ltype_core true env +let pr_goal_concl_style_env env = pr_ltype_core true env let pr_ltype_env env = pr_ltype_core false env let pr_type_env env = pr_type_core false env @@ -262,7 +268,7 @@ let default_pr_goal gs = let preamb,thesis,penv,pc = mt (), mt (), pr_context_of env, - pr_ltype_env_at_top env (Goal.V82.concl sigma g) + pr_goal_concl_style_env env (Goal.V82.concl sigma g) in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ @@ -279,7 +285,7 @@ let pr_goal_tag g = let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in - let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in + let pc = pr_goal_concl_style_env env (Goal.V82.concl sigma g) in str (emacs_str "") ++ str "subgoal " ++ int n ++ pr_goal_tag g ++ str " is:" ++ cut () ++ str" " ++ pc @@ -363,7 +369,8 @@ let default_pr_subgoals close_cmd sigma seeds = function let pei = pr_evars_int 1 exl in (str "No more subgoals but non-instantiated existential " ++ str "variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + str "You can use Grab Existential Variables.") end | [g] -> let pg = default_pr_goal { it = g ; sigma = sigma } in @@ -424,7 +431,7 @@ let pr_open_subgoals () = begin match bgoals with | [] -> pr_subgoals None sigma seeds goals | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++ - str"This subproof is complete, but there are still unfocused goals:" + str"This subproof is complete, but there are still unfocused goals." ++ fnl () (* spiwack: to stay compatible with the proof general and coqide, I use print the message after the goal. It would be better to have something like: |