diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_decl_mode.ml4 | 1 | ||||
| -rw-r--r-- | parsing/ppdecl_proof.ml | 1 | ||||
| -rw-r--r-- | parsing/printer.ml | 7 |
3 files changed, 3 insertions, 6 deletions
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 index 5c7b40afb..8942b6541 100644 --- a/parsing/g_decl_mode.ml4 +++ b/parsing/g_decl_mode.ml4 @@ -28,7 +28,6 @@ GLOBAL: proof_instr; thesis : [[ "thesis" -> Plain | "thesis"; "for"; i=ident -> (For i) - | "thesis"; "["; n=INT ;"]" -> (Sub (int_of_string n)) ]]; statement : [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml index ec8523d4d..9e3de9838 100644 --- a/parsing/ppdecl_proof.ml +++ b/parsing/ppdecl_proof.ml @@ -41,7 +41,6 @@ let pr_or_thesis pr_this env = function Thesis Plain -> str "thesis" | Thesis (For id) -> str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id - | Thesis (Sub n) -> str "thesis[" ++ int n ++ str "]" | This c -> pr_this env c let pr_cut pr_it env c = diff --git a/parsing/printer.ml b/parsing/printer.ml index c1a4415e3..7272ee697 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -262,16 +262,15 @@ let default_pr_goal g = pr_context_of env, pr_ltype_env_at_top env g.evar_concl else - let {pm_subgoals=metas} = get_info g in - (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), + (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), pr_context_of env, - pr_subgoal_metas metas env + pr_ltype_env_at_top env g.evar_concl in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ str "============================" ++ fnl () ++ - str" " ++ pc) ++ fnl () + str"thesis := " ++ fnl () ++ str " " ++ pc) ++ fnl () (* display the conclusion of a goal *) let pr_concl n g = |