Skip to content
Browse files

Update for r14789.

  • Loading branch information...
1 parent 7a90152 commit 56fec0937a131a97fa009f76fb188f1f0b0bde1a @tomprince committed Dec 18, 2011
Showing with 1 addition and 0 deletions.
  1. +1 −0 rippling_plugin.ml4
View
1 rippling_plugin.ml4
@@ -1406,6 +1406,7 @@ let lemma_cache ?(add_as_hint=true) prefix solving_tactic base g =
let ce =
{ Entries.const_entry_body = theorem_term;
const_entry_type = Some theorem_type;
+ const_entry_secctx = None;
const_entry_opaque = false}
in
ignore (Declare.declare_constant id (Entries.DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme)));

0 comments on commit 56fec09

Please sign in to comment.
Something went wrong with that request. Please try again.