diff options
| author | Emilio Jesus Gallego Arias | 2019-06-06 18:45:17 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-06 18:45:17 +0200 |
| commit | 20ee51330564b9ae6c3d3d0981db5184f99572ed (patch) | |
| tree | 2d85d3691d50602327de38fdb0caad6df976b759 | |
| parent | f841689a74a0456ecec63659ef5e7f568fb60ba0 (diff) | |
| parent | 3817bd950792da616eca03b6a9f2b706442227a7 (diff) | |
Merge PR #10278: vernac_load doesn't get a ?proof argument
Reviewed-by: ejgallego
Ack-by: gares
| -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 af13c873e2..8668f01053 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 |