From fd2d2a8178d78e441fb3191cf112ed517dc791af Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 May 2019 05:33:10 +0200
Subject: [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.
---
 vernac/classes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/classes.ml')

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
-- 
cgit v1.2.3