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

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 47645d295..8b4865594 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -340,6 +340,15 @@ let check_conv_leq_goal env sigma arg ty conclty =
       else raise (RefinerError (BadType (arg,ty,conclty)))
   else sigma
 
+exception Stop of constr list
+let meta_free_prefix a =
+  try
+    let _ = Array.fold_left (fun acc a -> 
+      if occur_meta a then raise (Stop acc)
+      else a :: acc) [] a
+    in a
+  with Stop acc -> Array.rev_of_list acc
+
 let goal_type_of env sigma c =
   if !check then type_of env sigma c
   else Retyping.get_type_of env sigma c
@@ -442,10 +451,10 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if isInd f || isConst f
-	     && not (Array.exists occur_meta l) (* we could be finer *)
+	  if is_template_polymorphic env f
 	  then
-	   (goalacc,type_of_global_reference_knowing_parameters env sigma f l,sigma,f)
+	    let l' = meta_free_prefix l in	      
+	   (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f)
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in