diff options
| author | Emilio Jesus Gallego Arias | 2019-05-22 05:33:10 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:54:43 +0200 |
| commit | fd2d2a8178d78e441fb3191cf112ed517dc791af (patch) | |
| tree | 8a85d441d2a25ad1ee4f46ef498694be9e9a8a12 /vernac/classes.ml | |
| parent | fb92bcc7830a084a4a204c4f58c44e83c180a9c9 (diff) | |
[proof] Remove duplicated universe polymorphic from decl_kinds
This information is already present on `Proof.t`, so we extract it
form there.
Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 37af8e1f55..bb5ebd7148 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -373,10 +373,10 @@ 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 kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in + let kind = Decl_kinds.Global ImportDefaultBehavior, Decl_kinds.DefinitionBody Decl_kinds.Instance in let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in let info = Lemmas.Info.make ~hook () in - let lemma = Lemmas.start_lemma ~name:id ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in + let lemma = Lemmas.start_lemma ~name:id ~poly ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in (* spiwack: I don't know what to do with the status here. *) let lemma = if not (Option.is_empty term) then |