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

diff --git a/kernel/environ.ml b/kernel/environ.ml
index dd4237b22..7a90f3675 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -311,17 +311,21 @@ let evaluable_constant kn env =
     | OpaqueDef _ -> false
     | Undef _ -> false
 
-let template_polymorphic_constant (cst,u) env =
-  if not (Univ.Instance.is_empty u) then false
-  else
-    match (lookup_constant cst env).const_type with 
-    | TemplateArity _ -> true
-    | RegularArity _ -> false
+let polymorphic_constant cst env =
+  (lookup_constant cst env).const_polymorphic
 
-let polymorphic_constant (cst,u) env =
+let polymorphic_pconstant (cst,u) env =
   if Univ.Instance.is_empty u then false
-  else
-    (lookup_constant cst env).const_polymorphic
+  else polymorphic_constant cst env
+
+let template_polymorphic_constant cst env =
+  match (lookup_constant cst env).const_type with 
+  | TemplateArity _ -> true
+  | RegularArity _ -> false
+
+let template_polymorphic_pconstant (cst,u) env =
+  if not (Univ.Instance.is_empty u) then false
+  else template_polymorphic_constant cst env
 
 let lookup_projection cst env =
   match (lookup_constant cst env).const_proj with 
@@ -336,17 +340,21 @@ let is_projection cst env =
 (* Mutual Inductives *)
 let lookup_mind = lookup_mind
 
-let template_polymorphic_ind ((mind,i),u) env =
-  if not (Univ.Instance.is_empty u) then false
-  else
-    match (lookup_mind mind env).mind_packets.(i).mind_arity with 
-    | TemplateArity _ -> true
-    | RegularArity _ -> false
+let polymorphic_ind (mind,i) env =
+  (lookup_mind mind env).mind_polymorphic
 
-let polymorphic_ind ((mind,i),u) env =
+let polymorphic_pind (ind,u) env =
   if Univ.Instance.is_empty u then false
-  else
-    (lookup_mind mind env).mind_polymorphic
+  else polymorphic_ind ind env
+
+let template_polymorphic_ind (mind,i) env =
+  match (lookup_mind mind env).mind_packets.(i).mind_arity with 
+  | TemplateArity _ -> true
+  | RegularArity _ -> false
+
+let template_polymorphic_pind (ind,u) env =
+  if not (Univ.Instance.is_empty u) then false
+  else template_polymorphic_ind ind env
   
 let add_mind_key kn mind_key env =
   let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in