- 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, 7 insertions, 7 deletions

diff --git a/library/library.ml b/library/library.ml
index dc712ce02c..d48f3b525c 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 =