diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-19 15:31:16 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-29 11:35:02 +0200 |
| commit | 848bc5b5fc366ab5869a2836c5ad83ab4d0f2842 (patch) | |
| tree | db2c2df53cb2b42dd6a41e1fbbe3b06aebe2f573 /vernac/lemmas.ml | |
| parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) | |
[vernac] Remove `Qed exporting` syntax.
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 4b36c2d07..192dd027c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -309,12 +309,6 @@ let get_proof proof do_guard hook opacity = in id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook -let check_exist = - List.iter (fun (loc,id) -> - if not (Nametab.exists_cci (Lib.make_path id)) then - user_err ?loc (pr_id id ++ str " does not exist.") - ) - let universe_proof_terminator compute_guard hook = let open Proof_global in make_terminator begin function @@ -322,17 +316,16 @@ let universe_proof_terminator compute_guard hook = admit (id,k,pe) pl (hook (Some ctx)) (); Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> - let is_opaque, export_seff, exports = match opaque with - | Vernacexpr.Transparent -> false, true, [] - | Vernacexpr.Opaque None -> true, false, [] - | Vernacexpr.Opaque (Some l) -> true, true, l in + let is_opaque, export_seff = match opaque with + | Vernacexpr.Transparent -> false, true + | Vernacexpr.Opaque -> true, false + in let proof = get_proof proof compute_guard (hook (Some (fst proof.Proof_global.universes))) is_opaque in begin match idopt with | None -> save_named ~export_seff proof | Some (_,id) -> save_anonymous ~export_seff proof id - end; - check_exist exports + end end let standard_proof_terminator compute_guard hook = |