aboutsummaryrefslogtreecommitdiff
path: root/plugins/derive
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-06-09 14:20:17 +0200
committerPierre-Marie Pédrot2019-06-09 14:20:17 +0200
commit1f81679d117446d32fcad8012e5613cb2377b359 (patch)
tree216bcc16b1cfce4d2a6ce1ce4356f3a5a7fffd0d /plugins/derive
parent73c2dc60ccd4d64506250a9c7476740e97ab022c (diff)
parent1c52097ecfccd22b7515f0e197b747107874b372 (diff)
Merge PR #8726: More robust treatment of the Discharge status
Reviewed-by: aspiwack Ack-by: ejgallego Reviewed-by: ppedrot
Diffstat (limited to 'plugins/derive')
-rw-r--r--plugins/derive/derive.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 9c1882dc9a..7c0f269481 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -26,7 +26,7 @@ let start_deriving f suchthat lemma =
let env = Global.env () in
let sigma = Evd.from_env env in
- let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in
+ let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in
(* create a sort variable for the type of [f] *)
(* spiwack: I don't know what the rigidity flag does, picked the one