diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 36e0fa23f..adc2054fe 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -35,6 +35,7 @@ open Tactics open Inv open Vernacexpr open Safe_typing +open Decl_kinds let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments" @@ -248,7 +249,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op = (DefinitionEntry { const_entry_body = invProof; const_entry_type = None; const_entry_opaque = false }, - Libnames.NeverDischarge) + IsProof Lemma) in () (* open Pfedit *) |