aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_utils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac_utils.ml')
-rw-r--r--plugins/subtac/subtac_utils.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 7fba23dc23..6487a14b7f 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -218,13 +218,13 @@ let non_instanciated_map env evd evm =
Evd.empty (Evarutil.non_instantiated evm)
let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
-let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let goal_kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Definition
let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
-let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
+let goal_proof_kind = Decl_kinds.Global, false, Decl_kinds.Proof Decl_kinds.Lemma
let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
-let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
+let goal_fix_kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
open Tactics
open Tacticals