- 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

1 files changed, 4 insertions, 2 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 4363ec442..55868097f 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