aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-05-19 15:31:16 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-09-29 11:35:02 +0200
commit848bc5b5fc366ab5869a2836c5ad83ab4d0f2842 (patch)
treedb2c2df53cb2b42dd6a41e1fbbe3b06aebe2f573 /plugins
parentb9740771e8113cb9e607793887be7a12587d0326 (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 'plugins')
-rw-r--r--plugins/funind/recdef.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d43fd78f3..7b63366e8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1288,8 +1288,8 @@ let build_new_goal_type () =
let is_opaque_constant c =
let cb = Global.lookup_constant c in
match cb.Declarations.const_body with
- | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None
- | Declarations.Undef _ -> Vernacexpr.Opaque None
+ | Declarations.OpaqueDef _ -> Vernacexpr.Opaque
+ | Declarations.Undef _ -> Vernacexpr.Opaque
| Declarations.Def _ -> Vernacexpr.Transparent
let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =