diff options
| author | Pierre-Marie Pédrot | 2019-09-29 16:13:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-29 16:13:40 +0200 |
| commit | 41f3d8f0b0b6efbb7133cd4e44c70a1d9105c3e9 (patch) | |
| tree | 750554abbd024ea720dd4ebafbc9751f5d62325c /vernac/classes.ml | |
| parent | 884b413e91d293a6b2009da11f2996db0654e40f (diff) | |
| parent | 10b54c11e2db436ab077477fae862fe06e0d9395 (diff) | |
Merge PR #10673: [lemmas] Cleanup users of default proof information.
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index d5f5656e1d..0a8c4e6b0f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -371,10 +371,9 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t the refinement manually.*) let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in - let scope = DeclareDef.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Instance) in let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in - let info = Lemmas.Info.make ~hook ~scope ~kind () in + let info = Lemmas.Info.make ~hook ~kind () in let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in (* spiwack: I don't know what to do with the status here. *) let lemma = |