Skip to content

Commit

Permalink
Cleanup vernac_check_guard
Browse files Browse the repository at this point in the history
Guard checking stop raising UserError a long time ago.
  • Loading branch information
SkySkimmer committed Apr 25, 2023
1 parent e575e94 commit 4c4c43a
Showing 1 changed file with 5 additions and 10 deletions.
15 changes: 5 additions & 10 deletions vernac/vernacentries.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2103,16 +2103,11 @@ let vernac_show ~pstate =
let vernac_check_guard ~pstate =
let pts = Declare.Proof.get pstate in
let pfterm = List.hd (Proof.partial_proof pts) in
let message =
try
let { Proof.entry; Proof.sigma } = Proof.data pts in
let hyps, _, _ = List.hd (Proofview.initial_goals entry) in
let env = Environ.reset_with_named_context hyps (Global.env ()) in
Inductiveops.control_only_guard env sigma pfterm;
(str "The condition holds up to here")
with UserError s ->
(str ("Condition violated: ") ++ s ++ str ".")
in message
let { Proof.entry; Proof.sigma } = Proof.data pts in
let hyps, _, _ = List.hd (Proofview.initial_goals entry) in
let env = Environ.reset_with_named_context hyps (Global.env ()) in
Inductiveops.control_only_guard env sigma pfterm;
str "The condition holds up to here."

let translate_vernac_synterp ?loc ~atts v = let open Vernacextend in match v with
| EVernacNotation { local; decl } ->
Expand Down

0 comments on commit 4c4c43a

Please sign in to comment.