Cleanup treatment of template universe polymorphism (thanks to E. Tassi

for helping fixing this).

Now the issue is handled solely through refreshing of the terms assigned
to evars during unification.
If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention
a template universe and in turn, ?X won't. Same goes when typechecking
(nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh
universes for the lists carriers. This also handles user-defined functions
on template polymorphic inductives, which was fragile before.
Pretyping and Evd are now uncluttered from template-specific code.

12 files changed, 102 insertions, 148 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 94ec09db2..b5aeeae3a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1559,7 +1559,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
         map_constr_with_full_binders push_binder aux x t
     | Evar ev ->
         let ty = get_type_of env sigma t in
-	let ty = Evarutil.evd_comb1 (refresh_universes false) evdref ty in
+	let ty = Evarutil.evd_comb1 (refresh_universes false env) evdref ty in
         let inst =
 	  List.map_i
 	    (fun i _ ->
@@ -1577,7 +1577,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
       let vl = List.map pi1 good in
       let ty = 
 	let ty = get_type_of env !evdref t in
-	  Evarutil.evd_comb1 (refresh_universes false) evdref ty
+	  Evarutil.evd_comb1 (refresh_universes false env) evdref ty
       in
       let ty = lift (-k) (aux x ty) in
       let depvl = free_rels ty in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 66d65bab6..26e96af48 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -26,23 +26,72 @@ let normalize_evar evd ev =
   | Evar (evk,args) -> (evk,args)
   | _ -> assert false
 
-let refresh_universes ?(all=false) ?(template=false) ?(with_globals=false) dir evd t =
+let get_polymorphic_positions f = 
+  let open Declarations in
+  match kind_of_term f with
+  | Ind (ind, u) | Construct ((ind, _), u) -> 
+    let mib,oib = Global.lookup_inductive ind in
+      (match oib.mind_arity with
+      | RegularArity _ -> assert false
+      | TemplateArity templ -> templ.template_param_levels)
+  | Const (cst, u) ->
+    let cb = Global.lookup_constant cst in
+      (match cb.const_type with
+      | RegularArity _ -> assert false
+      | TemplateArity (_, templ) -> 
+        templ.template_param_levels)
+  | _ -> assert false
+
+let refresh_universes dir env evd t =
   let evdref = ref evd in
   let modified = ref false in
-  let rec refresh dir t = match kind_of_term t with
-    | Sort (Type u as s) when Univ.universe_level u = None
-			 || (with_globals && Evd.is_sort_variable evd s = None) ->
-      (modified := true;
-       (* s' will appear in the term, it can't be algebraic *)
-       let s' = evd_comb0 (new_sort_variable ~template Evd.univ_flexible) evdref in
-	 evdref :=
-	   (if dir then set_leq_sort !evdref s' s else
-	     set_leq_sort !evdref s s');
-         mkSort s')
-    | Prod (na,u,v) -> mkProd (na,(if all then refresh true u else u),refresh dir v)
-    | _ -> t in
-  let t' = refresh dir t in
-  if !modified then !evdref, t' else evd, t
+  let rec refresh dir t = 
+    match kind_of_term t with
+    | Sort (Type u as s) when
+      (match Univ.universe_level u with
+      | None -> true 
+      | Some l -> Option.is_empty (Evd.is_sort_variable evd s)) ->
+      (* s' will appear in the term, it can't be algebraic *)
+      let s' = evd_comb0 (new_sort_variable Evd.univ_flexible) evdref in
+      let evd = 
+	if dir then set_leq_sort !evdref s' s
+	else set_leq_sort !evdref s s'
+      in
+	modified := true; evdref := evd; mkSort s'
+    | Prod (na,u,v) -> 
+      mkProd (na,u,refresh dir v)
+    | _ -> t
+  (** Refresh the types of evars under template polymorphic references *)
+  and refresh_term_evars onevars t =
+    match kind_of_term t with
+    | App (f, args) when is_template_polymorphic env f ->
+      let pos = get_polymorphic_positions f in
+	refresh_polymorphic_positions args pos
+    | Evar (ev, a) when onevars ->
+      let evi = Evd.find !evdref ev in
+      let ty' = refresh true evi.evar_concl in
+	if !modified then 
+	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
+	else ()
+    | _ -> iter_constr (refresh_term_evars onevars) t
+  and refresh_polymorphic_positions args pos =
+    let rec aux i = function
+      | Some l :: ls -> 
+        if i < Array.length args then 
+	  ignore(refresh_term_evars true args.(i));
+        aux (succ i) ls
+      | None :: ls -> 
+        if i < Array.length args then 
+          ignore(refresh_term_evars false args.(i));
+	aux (succ i) ls
+      | [] -> ()
+    in aux 0 pos
+  in
+  let t' = 
+    if isArity t then refresh dir t 
+    else (refresh_term_evars false t; t)
+  in
+    if !modified then !evdref, t' else !evdref, t
 
 (************************)
 (* Unification results  *)
@@ -504,7 +553,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       let id = next_name_away na avoid in
       let evd,t_in_sign =
         let s = Retyping.get_sort_of env evd t_in_env in
-        let evd,ty_t_in_sign = refresh_universes false evd (mkSort s) in
+        let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd t_in_env 
           ty_t_in_sign sign filter inst_in_env in
       let evd,b_in_sign = match b with
@@ -523,7 +572,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   in
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
-    let evd,ty_t_in_sign = refresh_universes false evd (mkSort s) in
+    let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd,ev2_in_sign =
@@ -1387,7 +1436,7 @@ and evar_define conv_algo ?(choose=false) ?(dir=false) env evd pbty (evk,argsv a
     (* so we recheck acyclicity *)
     if occur_evar evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
-    let evd', body = refresh_universes dir evd' body in
+    let evd', body = refresh_universes dir env evd' body in
 (* Cannot strictly type instantiations since the unification algorithm
  * does not unify applications from left to right.
  * e.g problem f x == g y yields x==y and f==g (in that order)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 23ed6a2ef..988938272 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,9 +34,8 @@ type conv_fun_bool =
 val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
-val refresh_universes : ?all:bool (* Include domains of products *) -> 
-  ?template:bool -> (* Generate template fresh universe variables, to be instantiated eagerly *) 
-  ?with_globals:bool -> bool -> evar_map -> types -> evar_map * types
+val refresh_universes : bool (* direction: true for levels lower than the existing levels *) ->
+  env -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conv_fun_bool -> env ->  evar_map ->
   bool option -> existential_key -> constr array -> constr array -> evar_map
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a842134df..7fa6f46fb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -816,27 +816,3 @@ let lift_tycon n = Option.map (lift n)
 let pr_tycon env = function
     None -> str "None"
   | Some t -> Termops.print_constr_env env t
-
-open Declarations
-
-let get_template_constructor_type evdref (ind, i) n =
-  let mib,oib = Global.lookup_inductive ind in
-  let ar =
-    match oib.mind_arity with
-    | RegularArity _ -> assert false
-    | TemplateArity templ -> templ
-  in
-  let ty = oib.mind_user_lc.(pred i) in
-  let subst = Inductive.ind_subst (fst ind) mib Univ.Instance.empty in
-  let ty = substl subst ty in
-    ar.template_param_levels, ty
-
-let get_template_inductive_type evdref ind n =
-  let mib,oib = Global.lookup_inductive ind in
-  let ar =
-    match oib.mind_arity with
-    | RegularArity _ -> assert false
-    | TemplateArity templ -> templ
-  in
-  let ctx = oib.mind_arity_ctxt in
-    ar.template_param_levels, mkArity(ctx, Type ar.template_level)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 55171eb4c..c0708aa85 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -221,10 +221,3 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
 val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
 val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
-
-(* val get_template_constructor_type : evar_map ref -> constructor -> int -> types *)
-val get_template_constructor_type : evar_map ref -> constructor -> int -> 
-  (Univ.universe_level option list * types)
-
-val get_template_inductive_type : evar_map ref -> inductive -> int -> 
-  (Univ.universe_level option list * types)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d5aaf9df3..09e34c6aa 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -288,7 +288,6 @@ type evar_universe_context =
     uctx_univ_variables : Universes.universe_opt_subst;
       (** The local universes that are unification variables *)
     uctx_univ_algebraic : Univ.universe_set; 
-    uctx_univ_template : Univ.universe_set; 
     (** The subset of unification variables that
 	can be instantiated with algebraic universes as they appear in types 
 	and universe instances only. *)
@@ -301,7 +300,6 @@ let empty_evar_universe_context =
     uctx_local = Univ.ContextSet.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
-    uctx_univ_template = Univ.LSet.empty;
     uctx_universes = Univ.initial_universes;
     uctx_initial_universes = Univ.initial_universes }
 
@@ -332,8 +330,6 @@ 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_univ_template = 
-	  Univ.LSet.union ctx.uctx_univ_template ctx'.uctx_univ_template;
 	uctx_initial_universes = ctx.uctx_initial_universes;
 	uctx_universes = 
 	  if local == ctx.uctx_local then ctx.uctx_universes
@@ -356,8 +352,6 @@ 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_univ_template = 
-	  Univ.LSet.diff ctx'.uctx_univ_template ctx.uctx_univ_template;
 	uctx_universes = ctx.uctx_initial_universes;
 	uctx_initial_universes = ctx.uctx_initial_universes }
 
@@ -381,7 +375,7 @@ let instantiate_variable l b v =
 
 exception UniversesDiffer
 
-let process_universe_constraints univs vars alg templ cstrs =
+let process_universe_constraints univs vars alg cstrs =
   let vars = ref vars in
   let normalize = Universes.normalize_universe_opt_subst vars in
   let rec unify_universes fo l d r local =
@@ -414,8 +408,6 @@ let process_universe_constraints univs vars alg templ cstrs =
 			Univ.enforce_eq (Univ.Universe.make l) r local
 		      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
 		      levels local
-		else if Univ.LSet.mem rl templ && Univ.Universe.is_level l then
-		  unify_universes fo l Universes.UEq r local
 		else
 		  Univ.enforce_leq l r local
 	  else if d == Universes.ULub then
@@ -468,7 +460,7 @@ let add_constraints_context ctx cstrs =
   let vars, local' =
     process_universe_constraints ctx.uctx_universes
       ctx.uctx_univ_variables ctx.uctx_univ_algebraic
-      ctx.uctx_univ_template cstrs'
+      cstrs'
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
@@ -482,7 +474,7 @@ let add_universe_constraints_context ctx cstrs =
   let vars, local' = 
     process_universe_constraints ctx.uctx_universes 
       ctx.uctx_univ_variables ctx.uctx_univ_algebraic 
-      ctx.uctx_univ_template cstrs 
+      cstrs 
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
@@ -990,7 +982,7 @@ let merge_universe_subst evd subst =
 let with_context_set rigid d (a, ctx) = 
   (merge_context_set rigid d ctx, a)
 
-let uctx_new_univ_variable template rigid name
+let uctx_new_univ_variable rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = Universes.new_univ_level (Global.current_dirpath ()) in
   let ctx' = Univ.ContextSet.union ctx (Univ.ContextSet.singleton u) in
@@ -1002,28 +994,24 @@ let uctx_new_univ_variable template rigid name
 	if b then {uctx with uctx_univ_variables = uvars';
 	  uctx_univ_algebraic = Univ.LSet.add u avars}
 	else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in
-  let uctx'' = if template then 
-      {uctx' with uctx_univ_template = Univ.LSet.add u uctx'.uctx_univ_template}
-    else uctx'
-  in
   let names = 
     match name with
     | Some n -> UNameMap.add n u uctx.uctx_names
     | None -> uctx.uctx_names
   in
-    {uctx'' with uctx_names = names; uctx_local = ctx';
+    {uctx' with uctx_names = names; uctx_local = ctx';
       uctx_universes = Univ.add_universe u uctx.uctx_universes}, u
 
-let new_univ_level_variable ?(template=false) ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable template rigid name evd.universes in
+let new_univ_level_variable ?name rigid evd =
+  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?(template=false) ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable template rigid name evd.universes in
+let new_univ_variable ?name rigid evd =
+  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?(template=false) ?name rigid d =
-  let (d', u) = new_univ_variable ~template rigid ?name d in
+let new_sort_variable ?name rigid d =
+  let (d', u) = new_univ_variable rigid ?name d in
     (d', Type u)
 
 let make_flexible_variable evd b u =
@@ -1067,11 +1055,10 @@ let is_sort_variable evd s =
   match s with 
   | Type u -> 
     (match Univ.universe_level u with
-    | Some l -> 
+    | Some l as x -> 
       let uctx = evd.universes in
-      if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then 
-	Some (l, not (Univ.LMap.mem l uctx.uctx_univ_variables))
-      else None
+	if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x
+	else None
     | None -> None)
   | _ -> None
 
@@ -1193,7 +1180,6 @@ let refresh_undefined_univ_variables uctx =
   let uctx' = {uctx_names = uctx.uctx_names;
 	       uctx_local = ctx'; 
 	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
-	       uctx_univ_template = uctx.uctx_univ_template;
 	       uctx_universes = Univ.initial_universes;
 	       uctx_initial_universes = uctx.uctx_initial_universes } in
     uctx', subst
@@ -1218,7 +1204,6 @@ let normalize_evar_universe_context uctx =
 	    uctx_local = us'; 
 	    uctx_univ_variables = vars'; 
 	    uctx_univ_algebraic = algs';
-	    uctx_univ_template = uctx.uctx_univ_template;
 	    uctx_universes = universes;
 	    uctx_initial_universes = uctx.uctx_initial_universes }
 	in fixpoint uctx'
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 1393a33d3..b6db3c263 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -261,7 +261,6 @@ val drop_side_effects : evar_map -> evar_map
     Evar maps also keep track of the universe constraints defined at a given
     point. This section defines the relevant manipulation functions. *)
 
-val is_sort_variable : evar_map -> sorts -> bool
 val whd_sort_variable : evar_map -> constr -> constr
 val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
 val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
@@ -438,16 +437,15 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
 val normalize_evar_universe_context : evar_universe_context -> 
   evar_universe_context
 
-val new_univ_level_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
-val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option 
-(** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is 
-    not a sort variable declared in [evm] *)
+val is_sort_variable : evar_map -> sorts -> Univ.universe_level option 
+(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
+    not a local sort variable declared in [evm] *)
 val is_flexible_level : evar_map -> Univ.Level.t -> bool
 
-
 val whd_sort_variable : evar_map -> constr -> constr
 (* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *)
 val normalize_universe : evar_map -> Univ.universe -> Univ.universe
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6f8b407ae..1520e1a7e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -527,20 +527,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
       inh_conv_coerce_to_tycon loc env evdref j tycon
 
   | GApp (loc,f,args) ->
-    let univs, fj = 
-      match f with
-      | GRef (loc, ConstructRef (ind, i as cstr), u')
-      	  when Environ.template_polymorphic_ind ind env ->
-       (** We refresh the universes so as to enforce using <= instead of instantiating
-      	   an unkwown ?X with the template polymorphic type variable and destroying
-      	   template polymorphism.
-      	   e.g. when typechecking nil : Π A : Type n, list A, we don't
-      	   want n to be used as the fixed carrier level of the list, so we
-      	   refresh it preemptively. *)
-      	let univs, ty = Evarutil.get_template_constructor_type evdref cstr (List.length args) in
-      	  univs, make_judge (mkConstruct cstr) ty
-      | _ -> [], pretype empty_tycon env evdref lvar f 
-    in
+    let fj = pretype empty_tycon env evdref lvar f in
     let floc = loc_of_glob_constr f in
     let length = List.length args in
     let candargs =
@@ -563,7 +550,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	      with Not_found -> []
       else []
     in
-    let rec apply_rec env n resj univs candargs = function
+    let rec apply_rec env n resj candargs = function
       | [] -> resj
       | c::rest ->
 	let argloc = loc_of_glob_constr c in
@@ -571,15 +558,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
         let resty = whd_betadeltaiota env !evdref resj.uj_type in
       	  match kind_of_term resty with
 	  | Prod (na,c1,c2) ->
-	    let univs, tycon = 
-	      match univs with
-	      | Some _ :: l -> 
-		if is_GHole c then
-		  l, Some (evd_comb1 (Evarsolve.refresh_universes ~template:true
-					~with_globals:true true) evdref c1)
-		else l, Some c1
-	      | (None :: l) | l -> l, Some c1
-	    in
+	    let tycon = Some c1 in
 	    let hj = pretype tycon env evdref lvar c in
 	    let candargs, ujval =
 	      match candargs with
@@ -590,10 +569,8 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 		else [], j_val hj
 	    in
 	    let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in
-	      apply_rec env (n+1)
-		{ uj_val = value;
-		  uj_type = typ }
-		univs candargs rest
+	    let j = { uj_val = value; uj_type = typ } in
+	      apply_rec env (n+1) j candargs rest
 		
 	  | _ ->
 	    let hj = pretype empty_tycon env evdref lvar c in
@@ -601,7 +578,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 		(Loc.merge floc argloc) env !evdref
 	      	resj [hj]
     in
-    let resj = apply_rec env 1 fj univs candargs args in
+    let resj = apply_rec env 1 fj candargs args in
     let resj =
       match evar_kind_of_term !evdref resj.uj_val with
       | App (f,args) ->
@@ -611,30 +588,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	    let c = mkApp (f,Array.map (whd_evar sigma) args) in
 	    let t = Retyping.get_type_of env sigma c in
 	      make_judge c (* use this for keeping evars: resj.uj_val *) t
-	    (* else  *)
-	    (*   if is_template_polymorphic_constructor env f then *)
-	    (*     let ty = nf_evar !evdref resj.uj_type in *)
-	    (* 	if occur_existential resj.uj_type then *)
-	    (* 	(\* The type is not fully defined, e.g. list ?A where A : Type n  *)
-	    (* 	   for n the fixed template universe of lists. We don't want this *)
-	  (* 	   n to escape (e.g. by later taking typeof(list A) = Type n) when *)
-	  (* 	   instantiating other existentials. So we need to refresh the  *)
-	  (* 	   type of f and redo typechecking with this fresh type. *\) *)
-	  (* 	  match kind_of_term f with *)
-	  (* 	  | Construct ((ind, i as cstr,u)) -> *)
-	  (* 	  (\** We refresh the universes so as to enforce using <= instead of instantiating *)
-    	  (* 	      an unkwown ?X with the template polymorphic type variable and destroying *)
-    	  (* 	      template polymorphism. *)
-    	  (* 	      e.g. when typechecking nil : Π A : Type n, list A, we don't *)
-    	  (* 	      want n to be used as the fixed carrier level of the list, so we *)
-    	  (* 	      refresh it preemptively. *\) *)
-	  (* 	    evdref := initial_evd; *)
-	  (* 	    let ty = Evarutil.get_template_constructor_type evdref cstr in *)
-    	  (* 	    let fj = make_judge (mkConstruct cstr) ty in *)
-	  (* 	      typecheck_app fj *)
-	  (* 	  | _ -> assert false *)
-	  (* 	else make_judge resj.uj_val ty *)
-	    else resj
+	  else resj
       | _ -> resj 
     in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 2f34f7efe..7702355b8 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c =
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
-      Evarsolve.refresh_universes false !evdref j.uj_type
+      Evarsolve.refresh_universes false env !evdref j.uj_type
     else !evdref, j.uj_type
 
 let solve_evars env evdref c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 58296002f..4ad8f833e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -936,7 +936,7 @@ let w_coerce env evd mv c =
   w_coerce_to_type env evd c cty mvty
 
 let unify_to_type env sigma flags c status u =
-  let sigma, c = refresh_universes false sigma c in
+  let sigma, c = refresh_universes false env sigma c in
   let t = get_type_of env sigma (nf_meta sigma c) in
   let t = nf_betaiota sigma (nf_meta sigma t) in
     unify_0 env sigma CUMUL flags t u
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index a0ecdb756..c9d868c40 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -212,7 +212,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
        try rewrite <- (gleaf i); auto; try apply IHi; congruence.
   Qed.
 
-  Lemma rleaf : forall (i : key), remove i (Leaf : t A) = Leaf.
+  Lemma rleaf : forall (i : key), remove i Leaf = Leaf.
   Proof. destruct i; simpl; auto. Qed.
 
   Theorem grs:
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b3c052f01..d2aa48db9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -93,7 +93,7 @@ let typecheck_params_and_fields def id t ps nots fs =
 	 (match kind_of_term sred with
 	 | Sort s' -> 
 	   (match Evd.is_sort_variable !evars s' with
-	   | Some (l, _) -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; sred
+	   | Some l -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; sred
 	   | None -> s)
 	 | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
     | None ->