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

diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index bb56958851..6d48aaa4e3 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -384,11 +384,11 @@ let rec execute env cstr =
         let argst = execute_array env args in
 	let ft =
 	  match kind_of_term f with
-	  | Ind ind when Environ.template_polymorphic_ind ind env ->
+	  | Ind ind when Environ.template_polymorphic_pind ind env ->
 	      (* Template sort-polymorphism of inductive types *)
 	    let args = Array.map (fun t -> lazy t) argst in
 	      judge_of_inductive_knowing_parameters env ind args
-	  | Const cst when Environ.template_polymorphic_constant cst env ->
+	  | Const cst when Environ.template_polymorphic_pconstant cst env ->
 	      (* Template sort-polymorphism of constants *)
 	    let args = Array.map (fun t -> lazy t) argst in
 	      judge_of_constant_knowing_parameters env cst args