diff options
Diffstat (limited to 'plugins/decl_mode/decl_mode.ml')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 51 |
1 files changed, 25 insertions, 26 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 55742386..d169dc13 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,9 +9,9 @@ open Names open Term open Evd +open Errors open Util - let daimon_flag = ref false let set_daimon_flag () = daimon_flag:=true @@ -20,15 +20,13 @@ let get_daimon_flag () = !daimon_flag -(* Information associated to goals. *) -open Store.Field type split_tree= - Skip_patt of Idset.t * split_tree - | Split_patt of Idset.t * inductive * - (bool array * (Idset.t * split_tree) option) array + Skip_patt of Id.Set.t * split_tree + | Split_patt of Id.Set.t * inductive * + (bool array * (Id.Set.t * split_tree) option) array | Close_patt of split_tree - | End_patt of (identifier * (int * int)) + | End_patt of (Id.t * (int * int)) type elim_kind = EK_dep of split_tree @@ -48,7 +46,7 @@ type per_info = per_wf:recpath} type stack_info = - Per of Decl_expr.elim_type * per_info * elim_kind * identifier list + Per of Decl_expr.elim_type * per_info * elim_kind * Id.t list | Suppose_case | Claim | Focus_claim @@ -69,27 +67,27 @@ let mode_of_pftreestate pts = (* spiwack: it used to be "top_goal_..." but this should be fine *) let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in let goal = List.hd goals in - if info.get (Goal.V82.extra sigma goal) = None then - Mode_tactic - else - Mode_proof + match Store.get (Goal.V82.extra sigma goal) info with + | None -> Mode_tactic + | Some _ -> Mode_proof let get_current_mode () = - try + try mode_of_pftreestate (Pfedit.get_pftreestate ()) - with e when Errors.noncritical e -> Mode_none + with Proof_global.NoCurrentProof -> Mode_none let check_not_proof_mode str = - if get_current_mode () = Mode_proof then - error str + match get_current_mode () with + | Mode_proof -> error str + | _ -> () let get_info sigma gl= - match info.get (Goal.V82.extra sigma gl) with + match Store.get (Goal.V82.extra sigma gl) info with | None -> invalid_arg "get_info" | Some pm -> pm let try_get_info sigma gl = - info.get (Goal.V82.extra sigma gl) + Store.get (Goal.V82.extra sigma gl) info let get_stack pts = let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in @@ -102,11 +100,13 @@ let proof_cond = Proof.no_cond proof_focus let focus p = let inf = get_stack p in - Proof.focus proof_cond inf 1 p + Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1) -let unfocus = Proof.unfocus proof_focus +let unfocus () = + Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) -let maximal_unfocus = Proof_global.maximal_unfocus proof_focus +let maximal_unfocus () = + Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) let get_top_stack pts = try @@ -116,8 +116,7 @@ let get_top_stack pts = let info = get_info sigma gl in info.pm_stack -let get_last env = - try - let (id,_,_) = List.hd (Environ.named_context env) in id - with Invalid_argument _ -> error "no previous statement to use" +let get_last env = match Environ.named_context env with + | (id,_,_)::_ -> id + | [] -> error "no previous statement to use" |