From 05fc0542f6c7a15b9187a2a91beb0aa7a42bb2fa Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 12 Dec 2017 19:36:15 +0100
Subject: Remove the local polymorphic flag hack.

Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
---
 pretyping/typeclasses.ml  | 6 ++----
 pretyping/typeclasses.mli | 2 +-
 2 files changed, 3 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bc9990d026..f153b63410 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -87,7 +87,6 @@ type instance = {
   (* Sections where the instance should be redeclared,
      None for discard, Some 0 for none. *)
   is_global: int option;
-  is_poly: bool;
   is_impl: global_reference;
 }
 
@@ -97,7 +96,7 @@ let instance_impl is = is.is_impl
 
 let hint_priority is = is.is_info.Vernacexpr.hint_priority
 
-let new_instance cl info glob poly impl =
+let new_instance cl info glob impl =
   let global =
     if glob then Some (Lib.sections_depth ())
     else None
@@ -107,7 +106,6 @@ let new_instance cl info glob poly impl =
     { is_class = cl.cl_impl;
       is_info = info ;
       is_global = global ;
-      is_poly = poly;
       is_impl = impl }
 
 (*
@@ -420,7 +418,7 @@ let declare_instance info local glob =
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
       assert (not (isVarRef glob) || local);
-      add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
+      add_instance (new_instance tc info (not local) glob)
     | None -> ()
 
 let add_class cl =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 0cbe1c71c0..ee28ec173b 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -53,7 +53,7 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
+val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool ->
   global_reference -> instance
 val add_instance : instance -> unit
 val remove_instance : instance -> unit
-- 
cgit v1.2.3