diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 4 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 9 |
2 files changed, 8 insertions, 5 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 730051c1..da88d48d 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -75,9 +75,9 @@ let mode_of_pftreestate pts = Mode_proof let get_current_mode () = - try + try mode_of_pftreestate (Pfedit.get_pftreestate ()) - with _ -> Mode_none + with e when Errors.noncritical e -> Mode_none let check_not_proof_mode str = if get_current_mode () = Mode_proof then diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 72caeaed..ab161b35 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -381,7 +381,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 @@ -519,7 +519,10 @@ 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 e when Errors.noncritical e -> + error "No previous equality." + in let typ,lhs,rhs = decompose_eq last_id gls0 in let items_tac gls = match cut.cut_by with @@ -849,7 +852,7 @@ let build_per_info etype casee gls = let ind = try destInd hd - with _ -> + with e when Errors.noncritical e -> error "Case analysis must be done on an inductive object." in let mind,oind = Global.lookup_inductive ind in let nparams,index = |