aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml2
-rw-r--r--proofs/clenv.mli1
-rw-r--r--proofs/goal_select.ml1
-rw-r--r--proofs/logic.ml8
-rw-r--r--proofs/proof.ml23
-rw-r--r--proofs/proof_bullet.ml12
-rw-r--r--proofs/tacmach.ml12
-rw-r--r--proofs/tacmach.mli2
8 files changed, 29 insertions, 32 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index e466992721..b0eb8dc646 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -128,8 +128,6 @@ let mk_clenv_from_n gls n (c,cty) =
let mk_clenv_from gls = mk_clenv_from_n gls None
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t)
-
(******************************************************************)
(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 3fca967395..7213c9318c 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -46,7 +46,6 @@ val clenv_meta_type : clausenv -> metavariable -> types
val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
val mk_clenv_from_n :
Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
-val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv
val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
(** Refresh the universes in a clenv *)
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
index a6e27c238f..36b50d9e9f 100644
--- a/proofs/goal_select.ml
+++ b/proofs/goal_select.ml
@@ -56,7 +56,6 @@ let parse_goal_selector = function
let () = let open Goptions in
declare_string_option
{ optdepr = false;
- optname = "default goal selector" ;
optkey = ["Default";"Goal";"Selector"] ;
optread = begin fun () ->
Pp.string_of_ppcmds
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a361c4208e..bac13fcfc3 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -79,7 +79,7 @@ let check = ref false
let with_check = Flags.with_option check
let check_typability env sigma c =
- if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
+ if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma
(************************************************************************)
(************************************************************************)
@@ -363,7 +363,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
gl::goalacc, conclty, sigma, ev
| Cast (t,k, ty) ->
- check_typability env sigma ty;
+ let sigma = check_typability env sigma ty in
let sigma = check_conv_leq_goal env sigma trm ty conclty in
let res = mk_refgoals sigma goal goalacc ty t in
(* we keep the casts (in particular VMcast and NATIVEcast) except
@@ -430,13 +430,13 @@ and mk_hdgoals sigma goal goalacc trm =
Goal.V82.mk_goal sigma hyps concl in
match kind trm with
| Cast (c,_, ty) when isMeta c ->
- check_typability env sigma ty;
+ let sigma = check_typability env sigma ty in
let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in
let ev = EConstr.Unsafe.to_constr ev in
gl::goalacc,ty,sigma,ev
| Cast (t,_, ty) ->
- check_typability env sigma ty;
+ let sigma = check_typability env sigma ty in
mk_refgoals sigma goal goalacc ty t
| App (f,l) ->
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5ab4409f8b..7d0b31734e 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -69,19 +69,16 @@ exception FullyUnfocused
let _ = CErrors.register_handler begin function
| CannotUnfocusThisWay ->
- CErrors.user_err 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 ->
- CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+ Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
| NoSuchGoals (i,j) ->
- CErrors.user_err ~hdr:"Focus" Pp.(
- str"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 ->
- CErrors.user_err
- ~hdr:"Focus"
- Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
- | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
- | _ -> raise CErrors.Unhandled
+ Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
+ | FullyUnfocused ->
+ Some (Pp.str "The proof is not focused")
+ | _ -> None
end
let check_cond_kind c k =
@@ -328,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 66e2ae5c29..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
- CErrors.user_err ~hdr:"Focus" Pp.(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 *)
@@ -179,7 +179,6 @@ let current_behavior = ref Strict.strict
let () =
Goptions.(declare_string_option {
optdepr = false;
- optname = "bullet behavior";
optkey = ["Bullet";"Behavior"];
optread = begin fun () ->
(!current_behavior).name
@@ -204,8 +203,7 @@ exception SuggestNoSuchGoals of int * Proof.t
let _ = CErrors.register_handler begin function
| SuggestNoSuchGoals(n,proof) ->
let suffix = suggest proof in
- CErrors.user_err
- 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) *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:04:22 +0000