diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 23:43:55 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-23 23:41:08 +0200 |
| commit | 10b54c11e2db436ab077477fae862fe06e0d9395 (patch) | |
| tree | 3cd3892d568e1a9c71b883a638c25455ff62bc5d /vernac | |
| parent | b0a9cbeaf0530533008aa99246164b2bad896c5a (diff) | |
[lemmas] Cleanup users of default proof information.
We remove calls of `Lemmas.Info.make` that where using the default
parameters, as this is mostly dead code now.
This brings into question quite a few things, in particular, the
uneven support of `scope` attributes by different commands / plugins.
We don't attempt to solve that yet, hopefully the ongoing constant
saving path refactoring will be able to take care of these
inconsistencies.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 3 | ||||
| -rw-r--r-- | vernac/obligations.ml | 7 |
2 files changed, 5 insertions, 5 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 075d89d0df..d3a591b203 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -373,10 +373,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 = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 37fe0df0ee..c0b722af09 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -397,8 +397,8 @@ let deps_remaining obls deps = deps [] -let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(IsDefinition Definition)) -let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(IsProof Lemma)) +let goal_kind = Decls.(IsDefinition Definition) +let goal_proof_kind = Decls.(IsProof Lemma) let kind_of_obligation o = match o with @@ -487,7 +487,8 @@ let rec solve_obligation prg num tac = ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); in let obl = subst_deps_obl obls obl in - let scope, kind = kind_of_obligation (snd obl.obl_status) in + let scope = DeclareDef.(Global Declare.ImportNeedQualified) in + let kind = kind_of_obligation (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in |