From 8dbfee5c5f897af8186cb1bdfb04fd4f88eca677 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 11 Mar 2015 16:29:19 +0100 Subject: Fix double print in decl_mode. After executing a command classified as VtProofStep the stm prints the goals (if used via the tty API). --- plugins/decl_mode/g_decl_mode.ml4 | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 03929b3b86..acec8ba4e8 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -65,23 +65,18 @@ let vernac_decl_proof () = else begin Decl_proof_instr.go_to_proof_mode () ; - Proof_global.set_proof_mode "Declarative" ; - Vernacentries.print_subgoals () + Proof_global.set_proof_mode "Declarative" end (* spiwack: some bureaucracy is not performed here *) let vernac_return () = begin Decl_proof_instr.return_from_tactic_mode () ; - Proof_global.set_proof_mode "Declarative" ; - Vernacentries.print_subgoals () + Proof_global.set_proof_mode "Declarative" end let vernac_proof_instr instr = - begin - Decl_proof_instr.proof_instr instr; - Vernacentries.print_subgoals () - end + Decl_proof_instr.proof_instr instr (* Before we can write an new toplevel command (see below) which takes a [proof_instr] as argument, we need to declare -- cgit v1.2.3 From 46957a5114fbc955f7c48d73cb0e02e932ddd520 Mon Sep 17 00:00:00 2001 From: Pierre Corbineau Date: Mon, 2 Mar 2015 14:42:12 +0100 Subject: rewiring Czar printers that were disabled Backported from trunk. --- plugins/decl_mode/decl_expr.mli | 32 +++---- plugins/decl_mode/g_decl_mode.ml4 | 12 +-- plugins/decl_mode/ppdecl_proof.ml | 169 +++++++++++++++++++++---------------- plugins/decl_mode/ppdecl_proof.mli | 14 ++- 4 files changed, 128 insertions(+), 99 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 7467604a60..3c4cacbc54 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -46,23 +46,23 @@ type ('constr,'tac) casee = Real of 'constr | Virtual of ('constr statement,'constr,'tac) cut -type ('hyp,'constr,'pat,'tac) bare_proof_instr = - | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr - | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr - | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr +type ('var,'constr,'pat,'tac) bare_proof_instr = + | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr + | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr + | Phence of ('var,'constr,'pat,'tac) bare_proof_instr | Pcut of ('constr or_thesis statement,'constr,'tac) cut | Prew of side * ('constr statement,'constr,'tac) cut - | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut - | Passume of ('hyp,'constr) hyp list - | Plet of ('hyp,'constr) hyp list - | Pgiven of ('hyp,'constr) hyp list - | Pconsider of 'constr*('hyp,'constr) hyp list + | Psuffices of ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut + | Passume of ('var,'constr) hyp list + | Plet of ('var,'constr) hyp list + | Pgiven of ('var,'constr) hyp list + | Pconsider of 'constr*('var,'constr) hyp list | Pclaim of 'constr statement | Pfocus of 'constr statement - | Pdefine of Id.t * 'hyp list * 'constr + | Pdefine of Id.t * 'var list * 'constr | Pcast of Id.t or_thesis * 'constr - | Psuppose of ('hyp,'constr) hyp list - | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) + | Psuppose of ('var,'constr) hyp list + | Pcase of 'var list*'pat*(('var,'constr or_thesis) hyp list) | Ptake of 'constr list | Pper of elim_type * ('constr,'tac) casee | Pend of block_type @@ -70,19 +70,19 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr = type emphasis = int -type ('hyp,'constr,'pat,'tac) gen_proof_instr= +type ('var,'constr,'pat,'tac) gen_proof_instr= {emph: emphasis; - instr: ('hyp,'constr,'pat,'tac) bare_proof_instr } + instr: ('var,'constr,'pat,'tac) bare_proof_instr } type raw_proof_instr = - ((Id.t*(Constrexpr.constr_expr option)) Loc.located, + ((Id.t * (Constrexpr.constr_expr option)) Loc.located, Constrexpr.constr_expr, Constrexpr.cases_pattern_expr, raw_tactic_expr) gen_proof_instr type glob_proof_instr = - ((Id.t*(Tacexpr.glob_constr_and_expr option)) Loc.located, + ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located, Tacexpr.glob_constr_and_expr, Constrexpr.cases_pattern_expr, Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index acec8ba4e8..2bd88d5aea 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -19,6 +19,7 @@ open Tok (* necessary for camlp4 *) open Pcoq.Constr open Pcoq.Tactic +open Ppdecl_proof let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in @@ -43,15 +44,6 @@ let pr_open_subgoals () = pr_subgoals close_cmd sigma goals *) -let pr_raw_proof_instr _ _ _ instr = - Errors.anomaly (Pp.str "Cannot print a proof_instr") - (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller - dans cette direction - Ppdecl_proof.pr_proof_instr (Global.env()) instr - *) -let pr_proof_instr _ _ _ instr = Empty.abort instr -let pr_glob_proof_instr _ _ _ instr = Empty.abort instr - let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr (Decl_mode.get_info sigma gl) @@ -87,7 +79,7 @@ let vernac_proof_instr instr = (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) (* Only declared at raw level, because only used in vernac commands. *) -let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type = +let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type = Genarg.make0 None "proof_instr" (* We create a new parser entry [proof_mode]. The Declarative proof mode diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 27308666d2..b3198dbf24 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -12,41 +12,35 @@ open Decl_expr open Names open Nameops -let pr_constr = Printer.pr_constr_env -let pr_tac = Pptactic.pr_glob_tactic -let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr - let pr_label = function Anonymous -> mt () | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () -let pr_constr env c = pr_constr env Evd.empty c - -let pr_justification_items env = function +let pr_justification_items pr_constr = function Some [] -> mt () | Some (_::_ as l) -> spc () ++ str "by" ++ spc () ++ - prlist_with_sep (fun () -> str ",") (pr_constr env) l + prlist_with_sep (fun () -> str ",") pr_constr l | None -> spc () ++ str "by *" -let pr_justification_method env = function +let pr_justification_method pr_tac = function None -> mt () | Some tac -> - spc () ++ str "using" ++ spc () ++ pr_tac env tac + spc () ++ str "using" ++ spc () ++ pr_tac tac -let pr_statement pr_it env st = - pr_label st.st_label ++ pr_it env st.st_it +let pr_statement pr_constr st = + pr_label st.st_label ++ pr_constr st.st_it -let pr_or_thesis pr_this env = function +let pr_or_thesis pr_this = function Thesis Plain -> str "thesis" | Thesis (For id) -> str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id - | This c -> pr_this env c + | This c -> pr_this c -let pr_cut pr_it env c = - hov 1 (pr_it env c.cut_stat) ++ - pr_justification_items env c.cut_by ++ - pr_justification_method env c.cut_using +let pr_cut pr_constr pr_tac pr_it c = + hov 1 (pr_it c.cut_stat) ++ + pr_justification_items pr_constr c.cut_by ++ + pr_justification_method pr_tac c.cut_using let type_or_thesis = function Thesis _ -> Term.mkProp @@ -54,128 +48,127 @@ let type_or_thesis = function let _I x = x -let rec print_hyps pconstr gtyp env sep _be _have hyps = +let rec pr_hyps pr_var pr_constr gtyp sep _be _have hyps = let pr_sep = if sep then str "and" ++ spc () else mt () in match hyps with (Hvar _ ::_) as rest -> spc () ++ pr_sep ++ str _have ++ - print_vars pconstr gtyp env false _be _have rest + pr_vars pr_var pr_constr gtyp false _be _have rest | Hprop st :: rest -> begin - let nenv = - match st.st_label with - Anonymous -> env - | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in - spc() ++ pr_sep ++ pr_statement pconstr env st ++ - print_hyps pconstr gtyp nenv true _be _have rest + (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) + spc() ++ pr_sep ++ pr_statement pr_constr st ++ + pr_hyps pr_var pr_constr gtyp true _be _have rest end | [] -> mt () -and print_vars pconstr gtyp env sep _be _have vars = +and pr_vars pr_var pr_constr gtyp sep _be _have vars = match vars with Hvar st :: rest -> begin - let nenv = - match st.st_label with - Anonymous -> anomaly (Pp.str "anonymous variable") - | Name id -> Environ.push_named (id,None,st.st_it) env in + (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ - pr_statement pr_constr env st ++ - print_vars pconstr gtyp nenv true _be _have rest + pr_var st ++ + pr_vars pr_var pr_constr gtyp true _be _have rest end | (Hprop _ :: _) as rest -> let _st = if _be then str "be such that" else str "such that" in - spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest + spc() ++ _st ++ pr_hyps pr_var pr_constr gtyp false _be _have rest | [] -> mt () -let pr_suffices_clause env (hyps,c) = - print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++ - str "to show" ++ spc () ++ pr_or_thesis pr_constr env c +let pr_suffices_clause pr_var pr_constr (hyps,c) = + pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++ + str "to show" ++ spc () ++ pr_or_thesis pr_constr c let pr_elim_type = function ET_Case_analysis -> str "cases" | ET_Induction -> str "induction" -let pr_casee env =function - Real c -> str "on" ++ spc () ++ pr_constr env c - | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut +let pr_block_type = function + B_elim et -> pr_elim_type et + | B_proof -> str "proof" + | B_claim -> str "claim" + | B_focus -> str "focus" + +let pr_casee pr_constr pr_tac =function + Real c -> str "on" ++ spc () ++ pr_constr c + | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut let pr_side = function Lhs -> str "=~" | Rhs -> str "~=" -let rec pr_bare_proof_instr _then _thus env = function +let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function | Pescape -> str "escape" - | Pthen i -> pr_bare_proof_instr true _thus env i - | Pthus i -> pr_bare_proof_instr _then true env i - | Phence i -> pr_bare_proof_instr true true env i + | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true _thus i + | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then true i + | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i | Pcut c -> begin match _then,_thus with false,false -> str "have" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c | false,true -> str "thus" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c | true,false -> str "then" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c | true,true -> str "hence" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c end | Psuffices c -> - str "suffices" ++ pr_cut pr_suffices_clause env c + str "suffices" ++ pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c | Prew (sid,c) -> (if _thus then str "thus" else str " ") ++ spc () ++ - pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c + pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c | Passume hyps -> - str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps + str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps | Plet hyps -> - str "let" ++ print_vars pr_constr _I env false true "let" hyps + str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps | Pclaim st -> - str "claim" ++ spc () ++ pr_statement pr_constr env st + str "claim" ++ spc () ++ pr_statement pr_constr st | Pfocus st -> - str "focus on" ++ spc () ++ pr_statement pr_constr env st + str "focus on" ++ spc () ++ pr_statement pr_constr st | Pconsider (id,hyps) -> - str "consider" ++ print_vars pr_constr _I env false false "consider" hyps - ++ spc () ++ str "from " ++ pr_constr env id + str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps + ++ spc () ++ str "from " ++ pr_constr id | Pgiven hyps -> - str "given" ++ print_vars pr_constr _I env false false "given" hyps + str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps | Ptake witl -> str "take" ++ spc () ++ - prlist_with_sep pr_comma (pr_constr env) witl + prlist_with_sep pr_comma pr_constr witl | Pdefine (id,args,body) -> str "define" ++ spc () ++ pr_id id ++ spc () ++ prlist_with_sep spc (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") args ++ spc () ++ - str "as" ++ (pr_constr env body) + pr_var st ++ str ")") args ++ spc () ++ + str "as" ++ (pr_constr body) | Pcast (id,typ) -> str "reconsider" ++ spc () ++ - pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ - str "as" ++ spc () ++ (pr_constr env typ) + pr_or_thesis pr_id id ++ spc () ++ + str "as" ++ spc () ++ (pr_constr typ) | Psuppose hyps -> str "suppose" ++ - print_hyps pr_constr _I env false false "we have" hyps + pr_hyps pr_var pr_constr _I false false "we have" hyps | Pcase (params,pat,hyps) -> str "suppose it is" ++ spc () ++ pr_pat pat ++ (if params = [] then mt () else (spc () ++ str "with" ++ spc () ++ prlist_with_sep spc (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") params ++ spc ())) + pr_var st ++ str ")") params ++ spc ())) ++ (if hyps = [] then mt () else (spc () ++ str "and" ++ - print_hyps (pr_or_thesis pr_constr) type_or_thesis - env false false "we have" hyps)) - | Pper (et,c) -> + pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis + false false "we have" hyps)) + | Pper (et,c) -> str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ - pr_casee env c - | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et - | _ -> anomaly (Pp.str "unprintable instruction") + pr_casee pr_constr pr_tac c + | Pend blk -> str "end" ++ spc () ++ pr_block_type blk let pr_emph = function 0 -> str " " @@ -184,7 +177,39 @@ let pr_emph = function | 3 -> str "*** " | _ -> anomaly (Pp.str "unknown emphasis") -let pr_proof_instr env instr = +let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr = pr_emph instr.emph ++ spc () ++ - pr_bare_proof_instr false false env instr.instr + pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr + + +let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) = + pr_gen_proof_instr + (fun (_,(id,otyp)) -> + match otyp with + None -> pr_id id + | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")" + ) + pconstr2 + Ppconstr.pr_cases_pattern_expr + (ptac Pptactic.ltop) + instr + +let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) = + pr_gen_proof_instr + (fun (_,(id,otyp)) -> + match otyp with + None -> pr_id id + | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")") + pconstr2 + Ppconstr.pr_cases_pattern_expr + (ptac Pptactic.ltop) + instr + +let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) = + pr_gen_proof_instr + (fun st -> pr_statement pconstr1 st) + pconstr2 + (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr) + (ptac Pptactic.ltop) + instr diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli index fd6fb66376..678fc07688 100644 --- a/plugins/decl_mode/ppdecl_proof.mli +++ b/plugins/decl_mode/ppdecl_proof.mli @@ -1,2 +1,14 @@ -val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds +open Decl_expr +open Pptactic + +val pr_gen_proof_instr : + ('var -> Pp.std_ppcmds) -> + ('constr -> Pp.std_ppcmds) -> + ('pat -> Pp.std_ppcmds) -> + ('tac -> Pp.std_ppcmds) -> + ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds + +val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer +val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer +val pr_proof_instr : proof_instr extra_genarg_printer -- cgit v1.2.3 From 2837753608c077b543467ad086d393dddf9c3f9d Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 3 Mar 2015 12:01:34 +0100 Subject: Declarative mode: fix the focus behaviour. I had previously mistakenly enforced the property that after solving every goal in a block, unfocusing was performed automatically until one goal is in focus. This is not how the declarative mode is supposed to behave. Rather every focus must be explicitely unfocused by a closing command. This hit a few bad interaction with the pure representation of proof introduced for the asynchronous processing. Some of the invariants seem fragile, so this minimally disruptive solution is probably not long-term. In particular since each block uses the same focus kind, an `end ` may close another block than intended if the number of unfocussing command executed is not the right one. --- plugins/decl_mode/decl_mode.ml | 6 ++++-- plugins/decl_mode/decl_proof_instr.ml | 35 ++++++++++++++++++++++------------- 2 files changed, 26 insertions(+), 15 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index d169dc1372..07bf6d3268 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -89,7 +89,7 @@ let get_info sigma gl= let try_get_info sigma gl = Store.get (Goal.V82.extra sigma gl) info -let get_stack pts = +let get_goal_stack pts = let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in let info = get_info sigma (List.hd goals) in info.pm_stack @@ -99,7 +99,7 @@ let proof_focus = Proof.new_focus_kind () let proof_cond = Proof.no_cond proof_focus let focus p = - let inf = get_stack p in + let inf = get_goal_stack p in Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1) let unfocus () = @@ -116,6 +116,8 @@ let get_top_stack pts = let info = get_info sigma gl in info.pm_stack +let get_stack pts = Proof.get_at_focus proof_focus pts + let get_last env = match Environ.named_context env with | (id,_,_)::_ -> id | [] -> error "no previous statement to use" diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index c61079e636..83dd10742d 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -131,12 +131,13 @@ let daimon_tac gls = (* post-instruction focus management *) -(* spiwack: This used to fail if there was no focusing command - above, but I don't think it ever happened. I hope it doesn't mess - things up*) let goto_current_focus () = - Decl_mode.maximal_unfocus () + Decl_mode.unfocus () +(* spiwack: used to catch errors indicating lack of "focusing command" + in the proof tree. In the current implementation, however, entering + the declarative mode puts a focus first, there should, therefore, + never be exception raised here. *) let goto_current_focus_or_top () = goto_current_focus () @@ -1444,12 +1445,19 @@ let rec postprocess pts instr = Type_errors.IllFormedRecBody(_,_,_,_,_)) -> anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end - | Pend _ -> - goto_current_focus_or_top () + | Pend (B_elim ET_Case_analysis) -> goto_current_focus () + | Pend _ -> () let do_instr raw_instr pts = let has_tactic = preprocess pts raw_instr.instr in - begin + (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the + current proof (and, actually so does [do_instr] later one, so + it's ok to do the same here. Ideally the proof should be properly + threaded through the commands here, but since the are interleaved + with actions on the proof mode, which is attached to the global + proof environment, it is not possible without heavy lifting. *) + let pts = Proof_global.give_me_the_proof () in + let pts = if has_tactic then let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in let gl = { it=List.hd gls ; sigma=sigma; } in @@ -1458,13 +1466,14 @@ let do_instr raw_instr pts = let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) env sigma glob_instr in - ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))) - else () end; + let (pts',_) = Proof.run_tactic (Global.env()) + (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in + pts' + else pts + in + Proof_global.simple_with_current_proof (fun _ _ -> pts); postprocess pts raw_instr.instr; - (* spiwack: this should restore a compatible semantics with - v8.3 where we never stayed focused on 0 goal. *) - Proof_global.set_proof_mode "Declarative" ; - Decl_mode.maximal_unfocus () + Proof_global.set_proof_mode "Declarative" let proof_instr raw_instr = let p = Proof_global.give_me_the_proof () in -- cgit v1.2.3 From caa1e9278136bbf2c9353eeb415d331eee99c172 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 12 Mar 2015 17:29:51 +0100 Subject: Declarative mode: remove a superfluous [set_proof_mode]. It was probably creating bugs when trying to use [escape]. --- plugins/decl_mode/decl_proof_instr.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 83dd10742d..ab5282e791 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1472,8 +1472,7 @@ let do_instr raw_instr pts = else pts in Proof_global.simple_with_current_proof (fun _ _ -> pts); - postprocess pts raw_instr.instr; - Proof_global.set_proof_mode "Declarative" + postprocess pts raw_instr.instr let proof_instr raw_instr = let p = Proof_global.give_me_the_proof () in -- cgit v1.2.3 From 71fcb53fd93edcac1925f97d619871e8597e24e2 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 12 Mar 2015 17:32:50 +0100 Subject: Declarative mode: remove dead code. --- plugins/decl_mode/decl_mode.ml | 3 --- plugins/decl_mode/decl_mode.mli | 2 -- 2 files changed, 5 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 07bf6d3268..da41cd86db 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -105,9 +105,6 @@ let focus p = let unfocus () = Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) -let maximal_unfocus () = - Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) - let get_top_stack pts = try Proof.get_at_focus proof_focus pts diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index 2864ba18ee..e12c4c9237 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -75,5 +75,3 @@ val get_last: Environ.env -> Id.t val focus : Proof.proof -> unit val unfocus : unit -> unit - -val maximal_unfocus : unit -> unit -- cgit v1.2.3 From edb3302188af4b5b75111339e3f466a6ec09aef2 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 12 Mar 2015 17:46:35 +0100 Subject: Declarative mode: make it so that unfocussing can only be done for closed subproofs. The front-end is supposed to take care of that, but it may help to catch bugs. --- plugins/decl_mode/decl_mode.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index da41cd86db..07df7c7f09 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -96,7 +96,7 @@ let get_goal_stack pts = let proof_focus = Proof.new_focus_kind () -let proof_cond = Proof.no_cond proof_focus +let proof_cond = Proof.done_cond proof_focus let focus p = let inf = get_goal_stack p in -- cgit v1.2.3