From 1ed00e4f8cded2a2024b66c3f7f4deee6ecd7c83 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 8 Nov 2013 11:31:22 +0100
Subject: - Fix bug preventing apply from unfolding Fixpoints. - Remove
 Universe Polymorphism flags everywhere. - Properly infer, discharge template
 arities and fix substitution inside them (kernel code to check for
 correctness). - Fix tactics that were supposing universe polymorphic
 constants/inductives to be parametric on that status. Required to make
 interp_constr* return the whole evar universe context now. - Fix the
 univ/level/instance hashconsing to respect the fact that marshalling doesn't
 preserve sharing, sadly losing most of its benefits. Short-term solution is
 to add hashes to these for faster comparison, longer term requires rewriting
 all serialization code.

Conflicts:
	kernel/univ.ml
	tactics/tactics.ml
	theories/Logic/EqdepFacts.v
---
 kernel/declareops.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 4363ec4428..55868097fe 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -47,12 +47,14 @@ let constraints_of_constant cb = Univ.Constraint.union
   (match cb.const_body with
   | Undef _ -> Univ.empty_constraint
   | Def c -> Univ.empty_constraint
-  | OpaqueDef o -> Univ.UContext.constraints (Opaqueproof.force_constraints o))
+  | OpaqueDef o -> Univ.ContextSet.constraints (Opaqueproof.force_constraints o))
 
 let universes_of_constant cb = 
   match cb.const_body with
   | Undef _ | Def _ -> cb.const_universes
-  | OpaqueDef o -> Opaqueproof.force_constraints o
+  | OpaqueDef o -> 
+    Univ.UContext.union cb.const_universes 
+      (Univ.ContextSet.to_context (Opaqueproof.force_constraints o))
 
 let universes_of_polymorphic_constant cb = 
   if cb.const_polymorphic then universes_of_constant cb
-- 
cgit v1.2.3