diff options
Diffstat (limited to 'proofs/decl_mode.ml')
| -rw-r--r-- | proofs/decl_mode.ml | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index 134a4d8b..8be5f355 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: decl_mode.ml 12422 2009-10-27 08:42:49Z corbinea $ i*) +(*i $Id$ i*) open Names open Term @@ -15,9 +15,9 @@ open Util let daimon_flag = ref false -let set_daimon_flag () = daimon_flag:=true +let set_daimon_flag () = daimon_flag:=true let clear_daimon_flag () = daimon_flag:=false -let get_daimon_flag () = !daimon_flag +let get_daimon_flag () = !daimon_flag type command_mode = Mode_tactic @@ -27,12 +27,12 @@ type command_mode = let mode_of_pftreestate pts = let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in if goal.evar_extra = None then - Mode_tactic + Mode_tactic else Mode_proof - + let get_current_mode () = - try + try mode_of_pftreestate (Pfedit.get_pftreestate ()) with _ -> Mode_none @@ -42,7 +42,7 @@ let check_not_proof_mode str = type split_tree= Skip_patt of Idset.t * split_tree - | Split_patt of Idset.t * inductive * + | Split_patt of Idset.t * inductive * (bool array * (Idset.t * split_tree) option) array | Close_patt of split_tree | End_patt of (identifier * (int * int)) @@ -54,7 +54,7 @@ type elim_kind = type recpath = int option*Declarations.wf_paths -type per_info = +type per_info = {per_casee:constr; per_ctype:types; per_ind:inductive; @@ -64,7 +64,7 @@ type per_info = per_nparams:int; per_wf:recpath} -type stack_info = +type stack_info = Per of Decl_expr.elim_type * per_info * elim_kind * identifier list | Suppose_case | Claim @@ -73,7 +73,7 @@ type stack_info = type pm_info = { pm_stack : stack_info list} -let pm_in,pm_out = Dyn.create "pm_info" +let pm_in,pm_out = Dyn.create "pm_info" let get_info gl= match gl.evar_extra with @@ -81,30 +81,30 @@ let get_info gl= | Some extra -> try pm_out extra with _ -> invalid_arg "get_info" -let get_stack pts = +let get_stack pts = let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in info.pm_stack -let get_top_stack pts = +let get_top_stack pts = let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in info.pm_stack let get_end_command pts = - match mode_of_pftreestate pts with + match mode_of_pftreestate pts with Mode_proof -> - Some + Some begin match get_top_stack pts with [] -> "\"end proof\"" | Claim::_ -> "\"end claim\"" | Focus_claim::_-> "\"end focus\"" - | (Suppose_case :: Per (et,_,_,_) :: _ - | Per (et,_,_,_) :: _ ) -> + | (Suppose_case :: Per (et,_,_,_) :: _ + | Per (et,_,_,_) :: _ ) -> begin match et with - Decl_expr.ET_Case_analysis -> + Decl_expr.ET_Case_analysis -> "\"end cases\" or start a new case" - | Decl_expr.ET_Induction -> + | Decl_expr.ET_Induction -> "\"end induction\" or start a new case" end | _ -> anomaly "lonely suppose" @@ -112,7 +112,7 @@ let get_end_command pts = | Mode_tactic -> begin try - ignore + ignore (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts); Some "\"return\"" with Not_found -> None @@ -120,8 +120,8 @@ let get_end_command pts = | Mode_none -> error "no proof in progress" -let get_last env = - try +let get_last env = + try let (id,_,_) = List.hd (Environ.named_context env) in id with Invalid_argument _ -> error "no previous statement to use" |