aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/tactics.ml4
2 files changed, 2 insertions, 4 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index c7b8e6cc0..d80e86241 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -233,7 +233,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let add_inversion_lemma name env sigma t sort dep inv_op =
let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
- let entry = definition_entry ~polymorphic:(Flags.use_polymorphic_flag ())
+ let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
~univs:(snd ctx) invProof in
let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
()
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 86c0b9dd5..9d0e9f084 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4888,9 +4888,7 @@ let anon_id = Id.of_string "anonymous"
let tclABSTRACT name_op tac =
let open Proof_global in
- let default_gk =
- { locality = Global; polymorphic = false; object_kind = Proof Theorem }
- in
+ let default_gk = (Global, false, Proof Theorem) in
let s, gk = match name_op with
| Some s ->
(try let _, gk, _ = current_proof_statement () in s, gk