diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.mli | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 19 |
3 files changed, 14 insertions, 9 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 1187d9d76..8c5aec38b 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -74,7 +74,7 @@ let mode_of_pftreestate pts = let get_current_mode () = try mode_of_pftreestate (Pfedit.get_pftreestate ()) - with _ -> Mode_none + with Proof_global.NoCurrentProof -> Mode_none let check_not_proof_mode str = if get_current_mode () = Mode_proof then diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index 538d8944d..c54dcdc28 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -70,6 +70,8 @@ val get_stack : Proof.proof -> stack_info list val get_top_stack : Proof.proof -> stack_info list val get_last: Environ.env -> Id.t +(** [get_last] raises a [UserError] when it cannot find a previous + statement in the environment. *) val focus : Proof.proof -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index dc51c2384..1ae8419c8 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -366,7 +366,7 @@ let find_subsubgoal c ctyp skip submetas gls = se.se_meta submetas se.se_meta_list} else dfs (pred n) - with _ -> + with e when Errors.noncritical e -> begin enstack_subsubgoals env se stack gls; dfs n @@ -451,11 +451,12 @@ let mk_stat_or_thesis info gls = function | Thesis Plain -> pf_concl gls let just_tac _then cut info gls0 = - let last_item = if _then then - let last_id = try get_last (pf_env gls0) with Failure _ -> - error "\"then\" and \"hence\" require at least one previous fact" in - [mkVar last_id] - else [] + let last_item = + if _then then + try [mkVar (get_last (pf_env gls0))] + with UserError _ -> + error "\"then\" and \"hence\" require at least one previous fact" + else [] in let items_tac gls = match cut.cut_by with @@ -504,7 +505,9 @@ let decompose_eq id gls = let instr_rew _thus rew_side cut gls0 = let last_id = - try get_last (pf_env gls0) with _ -> error "No previous equality." in + try get_last (pf_env gls0) + with UserError _ -> error "No previous equality." + in let typ,lhs,rhs = decompose_eq last_id gls0 in let items_tac gls = match cut.cut_by with @@ -834,7 +837,7 @@ let build_per_info etype casee gls = let ind = try destInd hd - with _ -> + with DestKO -> error "Case analysis must be done on an inductive object." in let mind,oind = Global.lookup_inductive ind in let nparams,index = |