- 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

8 files changed, 54 insertions, 27 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 97445755f..e92225637 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -126,7 +126,7 @@ let open_constant i ((sp,kn), obj) =
     | (Def _ | Undef _) -> ()
     | OpaqueDef lc ->
         match Opaqueproof.get_constraints lc with
-        | Some f when Future.is_val f -> Global.push_context (Future.force f)
+        | Some f when Future.is_val f -> Global.push_context_set (Future.force f)
         | _ -> ()
 
 let exists_name id =
@@ -196,7 +196,7 @@ let declare_constant_common id cst =
 
 let definition_entry ?(opaque=false) ?(inline=false) ?types 
     ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body =
-  { const_entry_body = Future.from_val (body,eff);
+  { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
     const_entry_proj = None;
@@ -216,8 +216,9 @@ let declare_sideff se =
   let id_of c = Names.Label.to_id (Names.Constant.label c) in
   let pt_opaque_of cb =
     match cb with
-    | { const_body = Def sc } -> Mod_subst.force_constr sc, false
-    | { const_body = OpaqueDef fc } -> Opaqueproof.force_proof fc, true
+    | { const_body = Def sc } -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false
+    | { const_body = OpaqueDef fc } -> 
+      (Opaqueproof.force_proof fc, Opaqueproof.force_constraints fc), true
     | { const_body = Undef _ } -> anomaly(str"Undefined side effect")
   in
   let ty_of cb =
diff --git a/library/declaremods.mli b/library/declaremods.mli
index a25247891..c5dc5a7f5 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -73,7 +73,7 @@ type library_objects
 val register_library :
   library_name ->
   Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
-  Univ.universe_context -> unit
+  Univ.universe_context_set -> unit
 
 val get_library_symbols_tbl : library_name -> Nativecode.symbol array
 
diff --git a/library/global.ml b/library/global.ml
index 74a2a1c0e..6c088e542 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -189,18 +189,38 @@ let type_of_global_in_context env r =
      let inst = Univ.UContext.instance univs in
        Inductive.type_of_constructor (cstr,inst) specif, univs
 
+let universes_of_global env r = 
+  let open Declarations in
+    match r with
+    | VarRef id -> Univ.UContext.empty
+    | ConstRef c -> 
+      let cb = Environ.lookup_constant c env in 
+	Declareops.universes_of_constant cb
+    | IndRef ind ->
+      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+	mib.mind_universes 
+    | ConstructRef cstr ->
+      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+	mib.mind_universes 
+
+let universes_of_global gr = 
+  universes_of_global (env ()) gr
+
 let is_polymorphic r = 
   let env = env() in 
   match r with
   | VarRef id -> false
-  | ConstRef c -> 
-     let cb = Environ.lookup_constant c env in cb.Declarations.const_polymorphic
-  | IndRef ind ->
-     let (mib, oib) = Inductive.lookup_mind_specif env ind in
-       mib.Declarations.mind_polymorphic
-  | ConstructRef cstr ->
-     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-       mib.Declarations.mind_polymorphic
+  | ConstRef c -> Environ.polymorphic_constant c env
+  | IndRef ind -> Environ.polymorphic_ind ind env
+  | ConstructRef cstr -> Environ.polymorphic_ind (inductive_of_constructor cstr) env
+
+let is_template_polymorphic r = 
+  let env = env() in 
+  match r with
+  | VarRef id -> false
+  | ConstRef c -> Environ.template_polymorphic_constant c env
+  | IndRef ind -> Environ.template_polymorphic_ind ind env
+  | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
 
 let current_dirpath () = 
   Safe_typing.current_dirpath (safe_env ())
diff --git a/library/global.mli b/library/global.mli
index 5995ff03f..de19e888c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -94,7 +94,7 @@ val start_library : DirPath.t -> module_path
 val export : DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
-  Safe_typing.compiled_library -> Univ.universe_context -> Safe_typing.vodigest ->
+  Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
   module_path * Nativecode.symbol array
 
 (** {6 Misc } *)
@@ -107,11 +107,15 @@ val env_of_context : Environ.named_context_val -> Environ.env
 val join_safe_environment : unit -> unit
 
 val is_polymorphic : Globnames.global_reference -> bool
+val is_template_polymorphic : Globnames.global_reference -> bool
 
 val type_of_global_in_context : Environ.env -> 
   Globnames.global_reference -> Constr.types Univ.in_universe_context
 val type_of_global_unsafe : Globnames.global_reference -> Constr.types 
 
+(** Returns the universe context of the global reference (whatever it's polymorphic status is). *)
+val universes_of_global : Globnames.global_reference -> Univ.universe_context
+
 (** {6 Retroknowledge } *)
 
 val register :
diff --git a/library/library.ml b/library/library.ml
index dc712ce02..d48f3b525 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -39,7 +39,7 @@ type library_t = {
   library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_imports : compilation_unit_name array;
   library_digests : Safe_typing.vodigest;
-  library_extra_univs : Univ.universe_context;
+  library_extra_univs : Univ.universe_context_set;
 }
 
 module LibraryOrdered = DirPath
@@ -329,7 +329,7 @@ type 'a table_status =
 let opaque_tables =
   ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t)
 let univ_tables =
-  ref (LibraryMap.empty : (Univ.universe_context table_status) LibraryMap.t)
+  ref (LibraryMap.empty : (Univ.universe_context_set table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -362,7 +362,7 @@ let access_univ_table dp i =
 module OpaqueTables = struct
 
  let a_constr = Future.from_val (Term.mkRel 1)
- let a_univ = Future.from_val Univ.UContext.empty
+ let a_univ = Future.from_val Univ.ContextSet.empty
  let a_discharge : Opaqueproof.cooking_info list = []
 
  let local_opaque_table = ref (Array.make 100 a_constr)
@@ -440,7 +440,7 @@ let () =
 
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.universe_context Future.computation array * Univ.universe_context * bool
+  Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
@@ -466,13 +466,13 @@ let intern_from_file f =
   add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
   let open Safe_typing in
   match univs with
-  | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.UContext.empty
+  | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
   | Some (utab,uall,true) ->
       add_univ_table lmd.md_name (Fetched utab);
       mk_library lmd (Dvivo (digest_lmd,digest_u)) uall
   | Some (utab,_,false) ->
       add_univ_table lmd.md_name (Fetched utab);
-      mk_library lmd (Dvo_or_vi digest_lmd) Univ.UContext.empty
+      mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
 
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
@@ -731,7 +731,7 @@ let save_library_to ?todo dir f =
     | Some d ->
         assert(!Flags.compilation_mode = Flags.BuildVi);
         f ^ "i", (fun x -> Some (d x)),
-          (fun x -> Some (x,Univ.UContext.empty,false)), (fun x -> Some x) in
+          (fun x -> Some (x,Univ.ContextSet.empty,false)), (fun x -> Some x) in
   Opaqueproof.reset_indirect_creator ();
   let cenv, seg, ast = Declaremods.end_library dir in
   let opaque_table, univ_table, disch_table, f2t_map =
diff --git a/library/library.mli b/library/library.mli
index fc043aab6..0f6f510d8 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -31,7 +31,7 @@ val require_library_from_file :
 (** Segments of a library *)
 type seg_lib
 type seg_univ = (* cst, all_cst, finished? *)
-  Univ.universe_context Future.computation array * Univ.universe_context * bool
+  Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
diff --git a/library/universes.ml b/library/universes.ml
index 138a248f0..5996d7a80 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -594,13 +594,12 @@ let normalize_context_set ctx us algs =
     let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
     (* Add equalities for globals which can't be merged anymore. *)
     let cstrs = LSet.fold (fun g cst -> 
-      Constraint.add (canon, Univ.Eq, g) cst) global cstrs 
+      Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid)
+      cstrs 
     in
-    (** Should this really happen? *)
-    let subst' = LSet.fold (fun f -> LMap.add f canon)
-      (LSet.union rigid flexible) LMap.empty
+    let subst = LSet.fold (fun f -> LMap.add f canon)
+      flexible subst
     in 
-    let subst = LMap.union subst' subst in
       (subst, cstrs))
     (LMap.empty, Constraint.empty) partition
   in
diff --git a/library/universes.mli b/library/universes.mli
index ab217e872..3b951997a 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -149,6 +149,9 @@ val constr_of_global : Globnames.global_reference -> constr
     anywhere. The constraints are forgotten as well. DO NOT USE in new code. *)
 val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context
 
+(** Returns the type of the global reference, by creating a fresh instance of polymorphic 
+    references and computing their instantiated universe context. (side-effect on the
+    universe counter, use with care). *)
 val type_of_global : Globnames.global_reference -> types in_universe_context_set
 
 (** Full universes substitutions into terms *)