diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 21 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
2 files changed, 17 insertions, 8 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7213727c2..99b2444c0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -534,11 +534,14 @@ let vernac_identity_coercion stre id qids qidt = (***********) (* Solving *) - -let vernac_solve n tcom = +let vernac_solve n tcom b = if not (refining ()) then error "Unknown command of the non proof-editing mode"; - solve_nth n (Tacinterp.hide_interp tcom); + begin + if b then + solve_nth n (Tacinterp.hide_interp tcom (get_end_tac ())) + else solve_nth n (Tacinterp.hide_interp tcom None) + end; print_subgoals(); (* in case a strict subtree was completed, go back to the top of the prooftree *) @@ -551,10 +554,16 @@ let vernac_solve n tcom = machine, and enables to instantiate existential variables when there are no more goals to solve. It cannot be a tactic since all tactics fail if there are no further goals to prove. *) - + let vernac_solve_existential = instantiate_nth_evar_com +let vernac_set_end_tac tac = + if not (refining ()) then + error "Unknown command of the non proof-editing mode"; + set_end_tac (Tacinterp.interp tac) + + (*****************************) (* Auxiliary file management *) @@ -1074,7 +1083,7 @@ let interp c = match c with | VernacIdentityCoercion (str,id,s,t) -> vernac_identity_coercion str id s t (* Solving *) - | VernacSolve (n,tac) -> vernac_solve n tac + | VernacSolve (n,tac,b) -> vernac_solve n tac b | VernacSolveExistential (n,c) -> vernac_solve_existential n c (* Auxiliary file and library management *) @@ -1129,7 +1138,7 @@ let interp c = match c with | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () | VernacDebug b -> vernac_debug b - + | VernacProof tac -> vernac_set_end_tac tac (* Toplevel control *) | VernacToplevelControl e -> raise e diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index adc46d2d1..a7ee9a57b 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -199,7 +199,7 @@ type vernac_expr = module_binder list * module_type_ast option (* Solving *) - | VernacSolve of int * raw_tactic_expr + | VernacSolve of int * raw_tactic_expr * bool | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) @@ -256,7 +256,7 @@ type vernac_expr = | VernacShow of showable | VernacCheckGuard | VernacDebug of bool - + | VernacProof of raw_tactic_expr (* Toplevel control *) | VernacToplevelControl of exn |