diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 18 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 10 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 12 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
4 files changed, 24 insertions, 18 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index e2ee5426b5..7d0b31734e 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -69,16 +69,16 @@ exception FullyUnfocused let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - Pp.str "This proof is focused, but cannot be unfocused this way" + Some (Pp.str "This proof is focused, but cannot be unfocused this way") | NoSuchGoals (i,j) when Int.equal i j -> - Pp.(str "[Focus] No such goal (" ++ int i ++ str").") + Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> - Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.") + Some Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.") | NoSuchGoal id -> - Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".") + Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".") | FullyUnfocused -> - Pp.str "The proof is not focused" - | _ -> raise CErrors.Unhandled + Some (Pp.str "The proof is not focused") + | _ -> None end let check_cond_kind c k = @@ -325,9 +325,9 @@ exception OpenProof of Names.Id.t option * open_error_reason let _ = CErrors.register_handler begin function | OpenProof (pid, reason) -> let open Pp in - Option.cata (fun pid -> - str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason - | _ -> raise CErrors.Unhandled + Some (Option.cata (fun pid -> + str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason) + | _ -> None end let warn_remaining_shelved_goals = diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 3ff0533b6b..d978885d62 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -79,8 +79,8 @@ module Strict = struct (function | FailedBullet (b,sugg) -> let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in - Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg) - | _ -> raise CErrors.Unhandled) + Some Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg) + | _ -> None) (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) @@ -203,7 +203,7 @@ exception SuggestNoSuchGoals of int * Proof.t let _ = CErrors.register_handler begin function | SuggestNoSuchGoals(n,proof) -> let suffix = suggest proof in - Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ - pr_non_empty_arg (fun x -> x) suffix) - | _ -> raise CErrors.Unhandled + Some (Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix)) + | _ -> None end diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index d3bce07814..3e4549f92c 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -76,7 +76,6 @@ let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce nf_betaiota let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) -let pf_unsafe_type_of = pf_reduce unsafe_type_of let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of @@ -117,9 +116,6 @@ module New = struct let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl - let pf_unsafe_type_of gl t = - pf_apply unsafe_type_of gl t - let pf_type_of gl t = pf_apply type_of gl t @@ -182,4 +178,12 @@ module New = struct let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t + + (* deprecated *) + let pf_unsafe_type_of gl t = + pf_apply (unsafe_type_of[@warning "-3"]) gl t + end + +(* deprecated *) +let pf_unsafe_type_of = pf_reduce unsafe_type_of[@warning "-3"] diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index aed1c89bfe..b4247f39b9 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,6 +34,7 @@ val pf_nth_hyp_id : Goal.goal sigma -> int -> Id.t val pf_last_hyp : Goal.goal sigma -> named_declaration val pf_ids_of_hyps : Goal.goal sigma -> Id.t list val pf_unsafe_type_of : Goal.goal sigma -> constr -> types +[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] val pf_type_of : Goal.goal sigma -> constr -> evar_map * types val pf_hnf_type_of : Goal.goal sigma -> constr -> types @@ -83,6 +84,7 @@ module New : sig (** WRONG: To be avoided at all costs, it typechecks the term entirely but forgets the universe constraints necessary to retypecheck it *) val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types + [@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] (** This function does no type inference and expects an already well-typed term. It recomputes its type in the fastest way possible (no conversion is ever involved) *) |