- 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

9 files changed, 33 insertions, 19 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 52e37e611..7fa11a918 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -273,6 +273,7 @@ type evar_universe_context =
 	can be instantiated with algebraic universes as they appear in types 
 	and universe instances only. *)
     uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
+    uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
   }
   
 let empty_evar_universe_context = 
@@ -280,11 +281,13 @@ let empty_evar_universe_context =
     uctx_postponed = Univ.UniverseConstraints.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
-    uctx_universes = Univ.initial_universes }
+    uctx_universes = Univ.initial_universes;
+    uctx_initial_universes = Univ.initial_universes }
 
 let evar_universe_context_from e c = 
-  {empty_evar_universe_context with 
-    uctx_local = c; uctx_universes = universes e}
+  let u = universes e in
+    {empty_evar_universe_context with 
+      uctx_local = c; uctx_universes = u; uctx_initial_universes = u}
 
 let is_empty_evar_universe_context ctx =
   Univ.ContextSet.is_empty ctx.uctx_local && 
@@ -305,11 +308,12 @@ let union_evar_universe_context ctx ctx' =
 	  Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
 	uctx_univ_algebraic = 
 	  Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
+	uctx_initial_universes = ctx.uctx_initial_universes;
 	uctx_universes = 
 	  if local == ctx.uctx_local then ctx.uctx_universes
 	  else
 	    let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-	      Univ.merge_constraints cstrsr ctx.uctx_universes}
+	      Univ.merge_constraints cstrsr ctx.uctx_universes }
 
 (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
 (* let union_evar_universe_context =  *)
@@ -325,7 +329,8 @@ let diff_evar_universe_context ctx' ctx  =
 	  Univ.LMap.diff ctx'.uctx_univ_variables ctx.uctx_univ_variables;
 	uctx_univ_algebraic = 
 	  Univ.LSet.diff ctx'.uctx_univ_algebraic ctx.uctx_univ_algebraic;
-	uctx_universes = Univ.empty_universes }
+	uctx_universes = Univ.empty_universes;
+	uctx_initial_universes = ctx.uctx_initial_universes }
 
 (* let diff_evar_universe_context_key = Profile.declare_profile "diff_evar_universe_context";; *)
 (* let diff_evar_universe_context = *)
@@ -334,6 +339,7 @@ let diff_evar_universe_context ctx' ctx  =
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
 let evar_universe_context_set ctx = ctx.uctx_local
+let evar_universe_context_constraints ctx = snd ctx.uctx_local
 let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local
 let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx }
 let evar_universe_context_subst ctx = ctx.uctx_univ_variables
@@ -916,7 +922,7 @@ let univ_flexible_alg = UnivFlexible true
 
 let evar_universe_context d = d.universes
 
-let get_universe_context_set d = d.universes.uctx_local
+let universe_context_set d = d.universes.uctx_local
 
 let universes evd = evd.universes.uctx_universes
 
@@ -1148,7 +1154,7 @@ let normalize_evar_universe_context_variables uctx =
   in
   let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
   (* let univs = subst_univs_universes subst uctx.uctx_universes in *)
-  let ctx_local', univs = Universes.refresh_constraints (Global.universes ()) ctx_local in
+  let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
     subst, { uctx with uctx_local = ctx_local';
       uctx_univ_variables = normalized_variables;
       uctx_universes = univs }
@@ -1191,7 +1197,8 @@ let refresh_undefined_univ_variables uctx =
   let uctx' = {uctx_local = ctx'; 
 	       uctx_postponed = Univ.UniverseConstraints.empty;(*FIXME*)
 	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
-	       uctx_universes = Univ.initial_universes} in
+	       uctx_universes = Univ.initial_universes;
+	       uctx_initial_universes = uctx.uctx_initial_universes } in
     uctx', subst
 
 let refresh_undefined_universes evd =
@@ -1218,7 +1225,7 @@ let normalize_evar_universe_context uctx =
       if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then 
         uctx
       else
-	let us', universes = Universes.refresh_constraints (Global.universes ()) us' in
+	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
 	(* let universes = subst_univs_opt_universes vars' uctx.uctx_universes in *)
 	let postponed = 
 	  Univ.subst_univs_universe_constraints (Universes.make_opt_subst vars') 
@@ -1229,7 +1236,8 @@ let normalize_evar_universe_context uctx =
 	    uctx_univ_variables = vars'; 
 	    uctx_univ_algebraic = algs';
 	    uctx_postponed = postponed;
-	    uctx_universes = universes} 
+	    uctx_universes = universes;
+	    uctx_initial_universes = uctx.uctx_initial_universes }
 	in fixpoint uctx'
   in fixpoint uctx
 
@@ -1254,6 +1262,7 @@ let nf_constraints =
   else nf_constraints
 
 let universes evd = evd.universes.uctx_universes
+let constraints evd = evd.universes.uctx_universes
 
 (* Conversion w.r.t. an evar map and its local universes. *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 020f0a7b4..9be18bc8a 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -415,6 +415,7 @@ type evar_universe_context
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
 val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
+val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
 val evar_context_universe_context : evar_universe_context -> Univ.universe_context
 val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
 val empty_evar_universe_context : evar_universe_context
@@ -427,6 +428,7 @@ val universes : evar_map -> Univ.universes
 val add_constraints_context : evar_universe_context -> 
   Univ.constraints -> evar_universe_context
 
+
 val normalize_evar_universe_context_variables : evar_universe_context -> 
   Univ.universe_subst in_evar_universe_context
 
@@ -458,7 +460,7 @@ val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool
 val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
 
 val evar_universe_context : evar_map -> evar_universe_context
-val get_universe_context_set : evar_map -> Univ.universe_context_set
+val universe_context_set : evar_map -> Univ.universe_context_set
 val universe_context : evar_map -> Univ.universe_context
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> Univ.universes
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3f14de282..18b96e765 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -875,7 +875,7 @@ let understand_judgment_tcc evdref env c =
 let ise_pretype_gen_ctx flags sigma env lvar kind c =
   let evd, c = ise_pretype_gen flags sigma env lvar kind c in
   let evd, f = Evarutil.nf_evars_and_universes evd in
-    f c, Evd.get_universe_context_set evd
+    f c, Evd.evar_universe_context evd
 
 (** Entry points of the high-level type synthesis algorithm *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 79b051845..72e9971d6 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -81,7 +81,7 @@ val understand_ltac : inference_flags ->
 (** Standard call to get a constr from a glob_constr, resolving implicit args *)
 
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
-  evar_map -> env -> glob_constr -> constr Univ.in_universe_context_set
+  evar_map -> env -> glob_constr -> constr Evd.in_evar_universe_context
 
 (** Idem but returns the judgment of the understood term *)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 676fc4f3a..b64156649 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -815,6 +815,9 @@ let local_whd_state_gen flags sigma =
 	  whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
 	|args, (Stack.Proj (n,m,p) :: s') ->
 	  whrec (Stack.nth args (n+m), s')
+	|args, (Stack.Fix (f,s',cst)::s'') ->
+          let x' = Stack.zip(x,args) in
+            whrec (contract_fix f cst, s' @ (Stack.append_app [|x'|] s''))
 	|_ -> s
       else s
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 27c1d252d..d728f1bff 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -870,8 +870,8 @@ let isGlobalRef c =
 
 let is_template_polymorphic env f =
   match kind_of_term f with
-  | Ind ind -> Environ.template_polymorphic_ind ind env
-  | Const c -> Environ.template_polymorphic_constant c env
+  | Ind ind -> Environ.template_polymorphic_pind ind env
+  | Const c -> Environ.template_polymorphic_pconstant c env
   | _ -> false
 
 let base_sort_cmp pb s0 s1 =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 6ef3d11da..8b4d02e04 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -194,7 +194,7 @@ val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
 val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) ->
   Reduction.conv_pb -> constr -> constr -> bool
 val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool
-val eq_constr : constr -> constr -> bool
+val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*)
 
 val eta_reduce_head : constr -> constr
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 339ca19fb..5cd05c58d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -207,12 +207,12 @@ let rec execute env evdref cstr =
         let jl = execute_array env evdref args in
 	let j =
 	  match kind_of_term f with
-	    | Ind ind when Environ.template_polymorphic_ind ind env ->
+	    | Ind ind when Environ.template_polymorphic_pind ind env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (inductive_type_knowing_parameters env ind
 		    (Evarutil.jv_nf_evar !evdref jl))
-	    | Const cst when Environ.template_polymorphic_constant cst env ->
+	    | Const cst when Environ.template_polymorphic_pconstant cst env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (constant_type_knowing_parameters env cst
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3bb3aa9ba..9e662150e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -603,7 +603,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	  expand curenvnb pb b wt substn cM f1 l1 cN f2 l2
 
   and reduce curenvnb pb b wt (sigma, metas, evars as substn) cM cN =
-    if not (subterm_restriction b flags) && use_full_betaiota flags then
+    if use_full_betaiota flags && not (subterm_restriction b flags) then
       let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
 	if not (eq_constr cM cM') then
 	  unirec_rec curenvnb pb b wt substn cM' cN