From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Sep 2017 14:50:07 +0200
Subject: When declaring constants/inductives use ContextSet if monomorphic.

Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.

There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
---
 plugins/ltac/rewrite.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f6523d28c2..a2f5a4577f 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1972,9 +1972,13 @@ let add_morphism_infer glob m n =
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
     if Lib.is_modtype () then
+      let uctx = if poly
+        then Entries.Polymorphic_const_entry (UState.context uctx)
+        else Entries.Monomorphic_const_entry (UState.context_set uctx)
+      in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
-				 (None,poly,(instance,UState.context uctx),None),
+                                 (None,(instance,uctx),None),
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
-- 
cgit v1.2.3