From 848bc5b5fc366ab5869a2836c5ad83ab4d0f2842 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 May 2017 15:31:16 +0200 Subject: [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. --- vernac/obligations.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/obligations.ml') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 89b18d254..81218308f 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -846,9 +846,9 @@ let obligation_terminator name num guard hook auto pf = let obl = obls.(num) in let status = match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp () - | (true, _), Vernacexpr.Opaque _ -> err_not_transp () - | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true + | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () + | (true, _), Vernacexpr.Opaque -> err_not_transp () + | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false | (_, status), Vernacexpr.Transparent -> status in -- cgit v1.2.3