diff options
| author | Gaëtan Gilbert | 2019-05-31 13:22:06 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-05 10:15:14 +0200 |
| commit | 3817bd950792da616eca03b6a9f2b706442227a7 (patch) | |
| tree | f307be0496b7d1e6e0e3d208bb180b7fc0713755 | |
| parent | c0a695e89b0562eb6450c04ddba5e6e0414e5fd8 (diff) | |
vernac_load doesn't get a ?proof argument
AFAICT the stm never gives Load a non-None ?proof.
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 18e0fde296..0f12959ae5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2694,7 +2694,7 @@ let rec interp_expr ?proof ~atts ~st c = [vernac_load] is mutually-recursive with [interp_expr] *) | VernacLoad (verbosely,fname) -> unsupported_attributes atts; - vernac_load ?proof ~verbosely ~st fname + vernac_load ~verbosely ~st fname (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *) | VernacEndProof e -> @@ -2711,7 +2711,7 @@ let rec interp_expr ?proof ~atts ~st c = the way the proof mode is set there makes the task non trivial without a considerable amount of refactoring. *) -and vernac_load ?proof ~verbosely ~st fname = +and vernac_load ~verbosely ~st fname = let pstate = st.Vernacstate.proof in if there_are_pending_proofs ~pstate then CErrors.user_err Pp.(str "Load is not supported inside proofs."); @@ -2734,7 +2734,7 @@ and vernac_load ?proof ~verbosely ~st fname = try let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) pstate in let pstate = - v_mod (interp_control ?proof ~st:{ st with Vernacstate.proof = pstate }) + v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.proof = pstate }) (parse_sentence proof_mode input) in load_loop ~pstate with |