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.
---
 plugins/ltac/rewrite.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac/rewrite.ml')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a698b05dd7..3cbb110010 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1981,8 +1981,7 @@ let add_morphism_infer glob m n =
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
-			(Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob
-			poly (ConstRef cst));
+                        (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
     else
       let kind = Decl_kinds.Global, poly, 
@@ -1993,7 +1992,7 @@ let add_morphism_infer glob m n =
 	| Globnames.ConstRef cst ->
 	  add_instance (Typeclasses.new_instance 
 			  (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
-			  glob poly (ConstRef cst));
+                          glob (ConstRef cst));
 	  declare_projection n instance_id (ConstRef cst)
 	| _ -> assert false
       in
-- 
cgit v1.2.3