diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.mli | 1 | ||||
| -rw-r--r-- | proofs/goal_select.ml | 1 | ||||
| -rw-r--r-- | proofs/logic.ml | 8 | ||||
| -rw-r--r-- | proofs/proof.ml | 15 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 8 |
6 files changed, 13 insertions, 22 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..e2ee5426b5 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -69,18 +69,15 @@ exception FullyUnfocused let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way") + 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").") + 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." - ) + 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") + Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".") + | FullyUnfocused -> + Pp.str "The proof is not focused" | _ -> raise CErrors.Unhandled end diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 66e2ae5c29..3ff0533b6b 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -79,7 +79,7 @@ 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) + Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg) | _ -> raise CErrors.Unhandled) @@ -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) + Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix) | _ -> raise CErrors.Unhandled end |