diff options
| -rw-r--r-- | kernel/term.mli | 2 | ||||
| -rw-r--r-- | lib/envars.ml | 5 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 2 | ||||
| -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 | ||||
| -rw-r--r-- | pretyping/classops.mli | 8 | ||||
| -rw-r--r-- | printing/prettyp.ml | 7 | ||||
| -rw-r--r-- | printing/printmod.ml | 4 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 4 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 |
12 files changed, 35 insertions, 24 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 65963e3e9..d180969a5 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -262,7 +262,7 @@ val is_small : sorts -> bool (** {6 Term destructors } *) (** Destructor operations are partial functions and - @raise [DestKO] if the term has not the expected form. *) + @raise DestKO if the term has not the expected form. *) exception DestKO diff --git a/lib/envars.ml b/lib/envars.ml index 84a41f8e4..cf3d6503d 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -36,9 +36,8 @@ let path_to_list p = let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in String.split sep p -let user_path () = - let path = try Sys.getenv "PATH" with _ -> raise Not_found in - path_to_list path +let user_path () = + path_to_list (Sys.getenv "PATH") (* may raise Not_found *) let rec which l f = match l with diff --git a/library/declaremods.mli b/library/declaremods.mli index 06446e2eb..d7121d6f6 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -125,7 +125,7 @@ val set_end_library_hook : (unit -> unit) -> unit (** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for - every object of the module. *) + every object of the module. Raises [Not_found] when [mp] is unknown. *) val really_import_module : module_path -> unit diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 3a2711622..20cf9edb8 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -123,7 +123,7 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= - try destApp (whd_delta env term) with _ -> raise Not_found in + try destApp (whd_delta env term) with DestKO -> raise Not_found in if eq_constr f (Lazy.force _eq) && (Array.length args)=3 then let patt1,rels1 = pattern_of_constr env sigma args.(1) 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 = diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 8f36e95e6..d0c7793ae 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -47,8 +47,12 @@ type coe_index type inheritance_path = coe_index list (** {6 Access to classes infos } *) -val class_info : cl_typ -> (cl_index * cl_info_typ) + val class_exists : cl_typ -> bool + +val class_info : cl_typ -> (cl_index * cl_info_typ) +(** @raise Not_found if this type is not a class *) + val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c] and its @@ -74,7 +78,9 @@ val coercion_exists : coe_typ -> bool val coercion_value : coe_index -> (unsafe_judgment * bool) (** {6 Lookup functions for coercion paths } *) + val lookup_path_between_class : cl_index * cl_index -> inheritance_path +(** @raise Not_found when no such path exists *) val lookup_path_between : env -> evar_map -> types * types -> types * types * inheritance_path diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f7f877ddf..4d7501ff9 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -266,7 +266,8 @@ let print_inductive_implicit_args = let print_inductive_renames = print_args_data_of_inductive_ids - (fun r -> try List.hd (Arguments_renaming.arguments_names r) with _ -> []) + (fun r -> + try List.hd (Arguments_renaming.arguments_names r) with Not_found -> []) ((!=) Anonymous) print_renames_list @@ -731,7 +732,7 @@ let print_coercions () = let index_of_class cl = try fst (class_info cl) - with _ -> + with Not_found -> errorlabstrm "index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") @@ -741,7 +742,7 @@ let print_path_between cls clt = let p = try lookup_path_between_class (i,j) - with _ -> + with Not_found -> errorlabstrm "index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") diff --git a/printing/printmod.ml b/printing/printmod.ml index 57d990b86..fd9b1f200 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -127,7 +127,7 @@ let print_body is_impl env mp (l,body) = try let env = Option.get env in Printer.pr_mutual_inductive_body env (MutInd.make2 mp l) mib - with _ -> + with e when Errors.noncritical e -> (if mib.mind_finite then str "Inductive " else str "CoInductive") ++ name) @@ -135,7 +135,7 @@ let print_struct is_impl env mp struc = begin (* If [mp] is a globally visible module, we simply import it *) try Declaremods.really_import_module mp - with _ -> + with Not_found -> (* Otherwise we try to emulate an import by playing with nametab *) let fp = nametab_register_dir mp in List.iter (nametab_register_body mp fp) struc diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 1b2ae9ec7..9d22b60e0 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -99,8 +99,8 @@ val cook_proof : (Proof.proof -> unit) -> val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit (** {6 ... } *) -(** [get_Proof.proof ()] returns the current focused pending proof or - raises [UserError "no focused proof"] *) +(** [get_pftreestate ()] returns the current focused pending proof or + @raise NoCurrentProof *) val get_pftreestate : unit -> Proof.proof diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 33a0bf98a..c1ca6a694 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -45,7 +45,7 @@ val set_proof_mode : string -> unit exception NoCurrentProof val give_me_the_proof : unit -> Proof.proof - +(** @raise NoCurrentProof when outside proof mode. *) (** [start_proof s str goals ~init_tac ~compute_guard hook] starts a proof of name [s] and |