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.
---
 API/API.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index def60ec267..682fef1fc1 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4331,7 +4331,7 @@ sig
   val class_info : Globnames.global_reference -> typeclass
   val mark_resolvables : ?filter:evar_filter -> Evd.evar_map -> Evd.evar_map
   val add_instance : instance -> unit
-  val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
+  val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool ->
                      Globnames.global_reference -> instance
 end
 
@@ -5798,7 +5798,7 @@ sig
   val lemInv_clause :
     Misctypes.quantified_hypothesis -> EConstr.constr -> Names.Id.t list -> unit Proofview.tactic
   val add_inversion_lemma_exn :
-    Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) ->
+    poly:bool -> Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) ->
     unit
 end
 
-- 
cgit v1.2.3