Merge branch 'v8.5'

37 files changed, 230 insertions, 89 deletions

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index 70889badc..20b7b5b53 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -8,7 +8,7 @@ eval `opam config env`
 make distclean
 OUTDIR=$PWD/_install
 DMGDIR=$PWD/_dmg
-./configure -debug -prefix $OUTDIR
+./configure -debug -prefix $OUTDIR -native-compiler no
 VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
 APP=bin/CoqIDE_${VERSION}.app
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b4375d4d6..8f8b29d10 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1026,6 +1026,10 @@ let map_metas_fvalue f evd =
   in
   set_metas evd (Metamap.smartmap map evd.metas)
 
+let map_metas f evd =
+  let map cl = map_clb f cl in
+  set_metas evd (Metamap.smartmap map evd.metas)
+
 let meta_opt_fvalue evd mv =
   match Metamap.find mv evd.metas with
     | Clval(_,b,_) -> Some b
diff --git a/engine/evd.mli b/engine/evd.mli
index d43d4f5f9..c8753b9c0 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -451,6 +451,7 @@ val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map
 
 val undefined_metas : evar_map -> metavariable list
 val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
+val map_metas : (constr -> constr) -> evar_map -> evar_map
 
 type metabinding = metavariable * constr * instance_status
 
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 0d9d021c6..44a62ef37 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -248,7 +248,7 @@ let dump_def ty loc secpath id =
 let dump_definition (loc, id) sec s =
   dump_def s loc (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
 
-let dump_constraint ((loc, n), _, _) sec ty =
+let dump_constraint (((loc, n),_), _, _) sec ty =
   match n with
     | Names.Name id -> dump_definition (loc, id) sec ty
     | Names.Anonymous -> ()
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 1443a2cd6..40812a3d8 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -130,7 +130,7 @@ and constr_notation_substitution =
     constr_expr list list * (** for recursive notations *)
     local_binder list list (** for binders subexpressions *)
 
-type typeclass_constraint = Name.t located * binding_kind * constr_expr
+type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr
 
 and typeclass_context = typeclass_constraint list
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ac665bc25..a8625009c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -340,7 +340,7 @@ let typecheck_inductive env mie =
 type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
-  | LocalNotConstructor of Context.Rel.t * constr list
+  | LocalNotConstructor of Context.Rel.t * int
   | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
@@ -359,11 +359,10 @@ let explain_ind_err id ntyp env nbpar c err =
     | LocalNotEnoughArgs kt ->
 	raise (InductiveError
 		 (NotEnoughArgs (env,c',mkRel (kt+nbpar))))
-    | LocalNotConstructor (paramsctxt,args)->
+    | LocalNotConstructor (paramsctxt,nargs)->
         let nparams = Context.Rel.nhyps paramsctxt in
 	raise (InductiveError
-		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,
-                                  List.length args - nparams)))
+		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,nargs)))
     | LocalNonPar (n,i,l) ->
 	raise (InductiveError
 		 (NonPar (env,c',n,mkRel i, mkRel (l+nbpar))))
@@ -587,7 +586,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
                 begin match hd with
                 | Rel j when Int.equal j (n + ntypes - i - 1) ->
                   check_correct_par ienv hyps (ntypes - i) largs
-                | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,largs)))
+                | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,nargs)))
                 end
               else
                 if not (List.for_all (noccur_between n ntypes) largs)
diff --git a/lib/flags.mli b/lib/flags.mli
index 62fa3b016..24780f0dc 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -90,6 +90,7 @@ val is_universe_polymorphism : unit -> bool
 val make_polymorphic_flag : bool -> unit
 val use_polymorphic_flag : unit -> bool
 
+val warn : bool ref
 val make_warn : bool -> unit
 val if_warn : ('a -> unit) -> 'a -> unit
 
diff --git a/library/declare.ml b/library/declare.ml
index 817870a7c..c59d190a0 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) =
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   let cst = Global.lookup_constant kn' in
-  add_section_constant (cst.const_proj <> None) kn' cst.const_hyps;
+  add_section_constant cst.const_polymorphic kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
   add_constant_kind (constant_of_kn kn) obj.cst_kind
 
@@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let kn' = Global.add_mind dir id mie in
   assert (eq_mind kn' (mind_of_kn kn));
   let mind = Global.lookup_mind kn' in
-  add_section_kn kn' mind.mind_hyps;
+  add_section_kn mind.mind_polymorphic kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
diff --git a/library/lib.ml b/library/lib.ml
index ff8929167..e4617cafb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -408,17 +408,24 @@ let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),
                 (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
+let check_same_poly p vars =
+  let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
+  if List.exists pred vars then
+    error "Cannot mix universe polymorphic and monomorphic declarations in sections."
+
 let add_section_variable id impl poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+       check_same_poly poly vars;
+       sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
 
 let add_section_context ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := (Context ctx :: vars,repl,abs)::sl
+       check_same_poly true vars;
+       sectab := (Context ctx :: vars,repl,abs)::sl
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
@@ -443,10 +450,11 @@ let instance_from_variable_context sign =
 
 let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx
   
-let add_section_replacement f g hyps =
+let add_section_replacement f g poly hyps =
   match !sectab with
   | [] -> ()
   | (vars,exps,abs)::sl ->
+    let () = check_same_poly poly vars in
     let sechyps,ctx = extract_hyps (vars,hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
     let subst, ctx = Univ.abstract_universes true ctx in
@@ -454,13 +462,13 @@ let add_section_replacement f g hyps =
     sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
 	      g (sechyps,subst,ctx) abs)::sl
 
-let add_section_kn kn =
+let add_section_kn poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
-    add_section_replacement f f
+    add_section_replacement f f poly
 
-let add_section_constant is_projection kn =
+let add_section_constant poly kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-    add_section_replacement f f
+    add_section_replacement f f poly
 
 let replacement_context () = pi2 (List.hd !sectab)
 
diff --git a/library/lib.mli b/library/lib.mli
index 53e98e760..e2e71ac90 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -178,9 +178,10 @@ val is_in_section : Globnames.global_reference -> bool
 
 val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
 val add_section_context : Univ.universe_context_set -> unit
-val add_section_constant : bool (* is_projection *) -> 
+val add_section_constant : Decl_kinds.polymorphic ->
   Names.constant -> Context.Named.t -> unit
-val add_section_kn : Names.mutual_inductive -> Context.Named.t -> unit
+val add_section_kn : Decl_kinds.polymorphic ->
+  Names.mutual_inductive -> Context.Named.t -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b7b9e2a6a..b5e9f9e06 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -189,7 +189,7 @@ let test_plural_form_types = function
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    record_field decl_notation rec_definition;
+    record_field decl_notation rec_definition pidentref;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
@@ -780,10 +780,10 @@ GEXTEND Gram
       | IDENT "transparent" -> Conv_oracle.transparent ] ]
   ;
   instance_name:
-    [ [ name = identref; sup = OPT binders ->
-	  (let (loc,id) = name in (loc, Name id)),
+    [ [ name = pidentref; sup = OPT binders ->
+	  (let ((loc,id),l) = name in ((loc, Name id),l)),
           (Option.default [] sup)
-      | -> (!@loc, Anonymous), []  ] ]
+      | -> ((!@loc, Anonymous), None), []  ] ]
   ;
   reserv_list:
     [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 0525ffb77..cf65262c4 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -287,6 +287,7 @@ module Prim =
 
     let name = Gram.entry_create "Prim.name"
     let identref = Gram.entry_create "Prim.identref"
+    let pidentref = Gram.entry_create "Prim.pidentref"
     let pattern_ident = Gram.entry_create "pattern_ident"
     let pattern_identref = Gram.entry_create "pattern_identref"
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a4b4bb22a..9b3a96975 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -173,6 +173,7 @@ module Prim :
     val ident : Id.t Gram.entry
     val name : Name.t located Gram.entry
     val identref : Id.t located Gram.entry
+    val pidentref : (Id.t located * (Id.t located list) option) Gram.entry
     val pattern_ident : Id.t Gram.entry
     val pattern_identref : Id.t located Gram.entry
     val base_ident : Id.t Gram.entry
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 92573a94f..fb45be663 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -156,7 +156,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	| Prod (n,t,c) ->
 	    let d = (n,None,t) in
 	    make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c)
-	| LetIn (n,b,t,c) ->
+	| LetIn (n,b,t,c) when List.is_empty largs ->
 	    let d = (n,Some b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
      	| Ind (_,_) ->
@@ -167,7 +167,10 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
                 base [|applist (mkRel (i+1), Context.Rel.to_extended_list 0 sign)|]
             else
 	      base
-      	| _ -> assert false
+      	| _ ->
+	   let t' = whd_betadeltaiota env sigma p in
+	   if Term.eq_constr p' t' then assert false
+	   else prec env i sign t'
     in
     prec env 0 []
   in
@@ -231,14 +234,17 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	| Prod (n,t,c) ->
 	    let d = (n,None,t) in
 	    mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
-	| LetIn (n,b,t,c) ->
+	| LetIn (n,b,t,c) when List.is_empty largs ->
 	    let d = (n,Some b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
      	| Ind _ ->
             let realargs = List.skipn nparrec largs
             and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in
             applist(lift i fk,realargs@[arg])
-     	| _ -> assert false
+     	| _ ->
+	   let t' = whd_betadeltaiota env sigma p in
+	     if Term.eq_constr t' p' then assert false
+	     else prec env i hyps t'
     in
     prec env 0 []
   in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6166fffbc..11fba7b94 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -133,12 +133,12 @@ let interp_universe_level_name evd (loc,s) =
 	 in evd, level
     else 
       try
-	let id =
-	  try Id.of_string s with _ -> raise Not_found in
-	  evd, Idmap.find id names
+	let level = Evd.universe_of_name evd s in
+	evd, level
       with Not_found ->
-	try let level = Evd.universe_of_name evd s in
-	      evd, level
+	try 
+	  let id = try Id.of_string s with _ -> raise Not_found in
+	  evd, Idmap.find id names
 	with Not_found -> 
 	  if not (is_strict_universe_declarations ()) then
   	    new_univ_level_variable ~name:s univ_rigid evd
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ccf470946..ffec926a8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -918,8 +918,9 @@ module Make
             hov 1 (
               (if abst then keyword "Declare" ++ spc () else mt ()) ++
                 keyword "Instance" ++
-                (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
-                    Anonymous -> mt ()) ++
+                (match instid with
+		 | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc () 
+                 | (_, Anonymous), _ -> mt ()) ++
                 pr_and_type_binders_arg sup ++
                 str":" ++ spc () ++
                 pr_constr cl ++ pr_priority pri ++
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f9b180de6..6caebf6c4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -82,11 +82,14 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
       let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
       let map c = Vars.subst_univs_level_constr subst c in
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in
-      (** FIXME: We're being inefficient here because we substitute the whole
-          evar map instead of just its metas, which are the only ones
-          mentioning the old universes. *)
-      Clenv.map_clenv map clenv, map c
+      (** Only metas are mentioning the old universes. *)
+      let clenv = {
+        templval = Evd.map_fl map clenv.templval;
+        templtyp = Evd.map_fl map clenv.templtyp;
+        evd = Evd.map_metas map evd;
+        env = Proofview.Goal.env gl;
+      } in
+      clenv, map c
     else
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 48b9006cd..97b5ba0cc 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -71,8 +71,11 @@ let instantiate_tac_by_name id c =
 let let_evar name typ =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
+    let sigma = ref sigma in
+    let _ = Typing.sort_of env sigma typ in
+    let sigma = Sigma.Unsafe.of_evar_map !sigma in
     let id = match name with
     | Names.Anonymous -> 
       let id = Namegen.id_of_name_using_hdchar env typ name in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index d14e7deff..29002af9e 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1707,7 +1707,7 @@ let rec strategy_of_ast = function
 let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l)
 
 let declare_an_instance n s args =
-  ((Loc.ghost,Name n), Explicit,
+  (((Loc.ghost,Name n),None), Explicit,
   CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None),
 	   args))
 
@@ -1923,7 +1923,7 @@ let add_morphism glob binders m s n =
   let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance =
-    ((Loc.ghost,Name instance_id), Explicit,
+    (((Loc.ghost,Name instance_id),None), Explicit,
     CAppExpl (Loc.ghost,
 	     (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
 	     [cHole; s; m]))
diff --git a/test-suite/bugs/closed/4378.v b/test-suite/bugs/closed/4378.v
new file mode 100644
index 000000000..9d5916556
--- /dev/null
+++ b/test-suite/bugs/closed/4378.v
@@ -0,0 +1,9 @@
+Tactic Notation "epose" open_constr(a) :=
+  let a' := fresh in
+  pose a as a'.
+Tactic Notation "epose2" open_constr(a) tactic3(tac) :=
+  let a' := fresh in
+  pose a as a'.
+Goal True.
+  epose _. Undo.
+  epose2 _ idtac.
diff --git a/test-suite/bugs/closed/4495.v b/test-suite/bugs/closed/4495.v
new file mode 100644
index 000000000..8b032db5f
--- /dev/null
+++ b/test-suite/bugs/closed/4495.v
@@ -0,0 +1 @@
+Fail Notation "'forall' x  ..  y ',' P " := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder).
diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v
new file mode 100644
index 000000000..f54d6433d
--- /dev/null
+++ b/test-suite/bugs/closed/4503.v
@@ -0,0 +1,37 @@
+Require Coq.Classes.RelationClasses.
+
+Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
+{ refl : forall x, r x x }.
+
+(* FAILURE 1 *)
+
+Section foo.
+  Polymorphic Universes A.
+  Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
+
+  Fail Definition foo := PO.
+End foo.
+
+
+Module ILogic.
+
+Set Universe Polymorphism.
+
+(* Logical connectives *)
+Class ILogic@{L} (A : Type@{L}) : Type := mkILogic
+{
+  lentails: A -> A -> Prop;
+  lentailsPre:> RelationClasses.PreOrder lentails
+}.
+
+
+End ILogic.
+
+Set Printing Universes.
+
+(* There is stil a problem if the class is universe polymorphic *)
+Section Embed_ILogic_Pre.
+  Polymorphic Universes A T.
+  Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
+
+End Embed_ILogic_Pre.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4511.v b/test-suite/bugs/closed/4511.v
new file mode 100644
index 000000000..0cdb3aee4
--- /dev/null
+++ b/test-suite/bugs/closed/4511.v
@@ -0,0 +1,3 @@
+Goal True.
+Fail evar I.
+
diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v
new file mode 100644
index 000000000..ccbc47d20
--- /dev/null
+++ b/test-suite/bugs/closed/4519.v
@@ -0,0 +1,21 @@
+Set Universe Polymorphism.
+Section foo.
+  Universe i.
+  Context (foo : Type@{i}) (bar : Type@{i}).
+  Definition qux@{i} (baz : Type@{i}) := foo -> bar.
+End foo.
+Set Printing Universes.
+Print qux. (* qux@{Top.42 Top.43} =
+fun foo bar _ : Type@{Top.42} => foo -> bar
+     : Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42}
+(* Top.42 Top.43 |=  *)
+(* This is wrong; the first two types are equal, but the last one is not *)
+
+qux is universe polymorphic
+Argument scopes are [type_scope type_scope type_scope]
+ *)
+Check qux nat nat nat : Set.
+Check qux nat nat Set : Set. (* Error:
+The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is 
+expected to have type "Set"
+(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v
index ba69f6b15..dba4d5998 100644
--- a/test-suite/bugs/closed/HoTT_coq_002.v
+++ b/test-suite/bugs/closed/HoTT_coq_002.v
@@ -9,7 +9,7 @@ Section SpecializedFunctor.
   (* Variable objC : Type. *)
   Context `(C : SpecializedCategory objC).
 
-  Polymorphic Record SpecializedFunctor := {
+  Record SpecializedFunctor := {
     ObjectOf' : objC -> Type;
     ObjectC : Object C
   }.
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index 4938b80f9..008fb72c4 100644
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -59,8 +59,8 @@ Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
   := Build_Functor Cat0 C (fun x => match x with end).
 
 Section Law0.
-  Variable objC : Type.
-  Variable C : Category objC.
+  Polymorphic Variable objC : Type.
+  Polymorphic Variable C : Category objC.
 
   Set Printing All.
   Set Printing Universes.
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 8ded74763..841f843c0 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -631,6 +631,8 @@ End NoRetractFromTypeToProp.
 
 Module TypeNeqSmallType.
 
+Unset Universe Polymorphism.
+
 Section Paradox.
 
 (** ** Universe [U] is equal to one of its elements. *)
@@ -655,7 +657,6 @@ Proof.
   reflexivity.
 Qed.
 
-
 Theorem paradox : False.
 Proof.
   Generic.paradox p.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index f9bff3ac9..147759f5f 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -99,7 +99,13 @@ let string_prefix a b =
 let is_prefix dir1 dir2 =
   let l1 = String.length dir1 in
   let l2 = String.length dir2 in
-    dir1 = dir2 || (l1 < l2 && String.sub dir2 0 l1 = dir1 && dir2.[l1] = '/')
+  let sep = Filename.dir_sep in
+  if dir1 = dir2 then true
+  else if l1 + String.length sep <= l2 then
+    let dir1' = String.sub dir2 0 l1 in
+    let sep' = String.sub dir2 l1 (String.length sep) in
+    dir1' = dir1 && sep' = sep
+  else false
 
 let physical_dir_of_logical_dir ldir =
   let le = String.length ldir - 1 in
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index f5eccbfa4..c63e4aaa6 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -489,15 +489,15 @@ let add_caml_known phys_dir _ f =
     | _ -> ()
 
 let add_coqlib_known recur phys_dir log_dir f =
-  match get_extension f [".vo"] with
-    | (basename,".vo") ->
+  match get_extension f [".vo"; ".vio"] with
+    | (basename, (".vo" | ".vio")) ->
         let name = log_dir@[basename] in
         let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
 let add_known recur phys_dir log_dir f =
-  match get_extension f [".v";".vo"] with
+  match get_extension f [".v"; ".vo"; ".vio"] with
     | (basename,".v") ->
 	let name = log_dir@[basename] in
 	let file = phys_dir//basename in
@@ -506,7 +506,7 @@ let add_known recur phys_dir log_dir f =
           let paths = List.tl (suffixes name) in
           let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
           List.iter iter paths
-    | (basename,".vo") when not(!option_boot) ->
+    | (basename, (".vo" | ".vio")) when not(!option_boot) ->
         let name = log_dir@[basename] in
 	let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 936343628..6bb047af0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -102,19 +102,21 @@ let instance_hook k pri global imps ?hook cst =
   Typeclasses.declare_instance pri (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant k pri global imps ?hook id poly uctx term termtype =
+let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype =
   let kind = IsDefinition Instance in
-  let uctx = 
+  let evm = 
     let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
 				 (Universes.universes_of_constr term) in
-      Universes.restrict_universe_context uctx levels 
+    Evd.restrict_universe_context evm levels 
   in
+  let pl, uctx = Evd.universe_context ?names:pl evm in
   let entry = 
-    Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term
+    Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
   in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
+    Universes.register_universe_binders (ConstRef kn) pl;
     instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
@@ -122,7 +124,9 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
     ?(generalize=true)
     ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
-  let evars = ref (Evd.from_env env) in
+  let ((loc, instid), pl) = instid in
+  let uctx = Evd.make_evar_universe_context env pl in
+  let evars = ref (Evd.from_ctx uctx) in
   let tclass, ids =
     match bk with
     | Implicit ->
@@ -159,7 +163,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
       cl, u, c', ctx', ctx, len, imps, args
   in
   let id =
-    match snd instid with
+    match instid with
 	Name id ->
 	  let sp = Lib.make_path id in
 	    if Nametab.exists_cci sp then
@@ -186,11 +190,13 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    nf t
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
-	let pl, ctx = Evd.universe_context !evars in
+	let pl, ctx = Evd.universe_context ?names:pl !evars in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
 	  (ParameterEntry 
             (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
-	in instance_hook k None global imps ?hook (ConstRef cst); id
+	in
+	  Universes.register_universe_binders (ConstRef cst) pl;
+	  instance_hook k None global imps ?hook (ConstRef cst); id
       end
     else (
       let props =
@@ -283,9 +289,8 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
       in
       let term = Option.map nf term in
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
-          let ctx = Evd.universe_context_set evm in
-	  declare_instance_constant k pri global imps ?hook id 
-            poly ctx (Option.get term) termtype
+	  declare_instance_constant k pri global imps ?hook id pl
+            poly evm (Option.get term) termtype
 	else if !refine_instance || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	    if Flags.is_program_mode () then
@@ -305,7 +310,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
               let hook = Lemmas.mk_hook hook in
 	      let ctx = Evd.evar_universe_context evm in
 		ignore (Obligations.add_definition id ?term:constr
-			typ ctx ~kind:(Global,poly,Instance) ~hook obls);
+ 			?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
 		id
 	    else
 	      (Flags.silently 
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 8dcfabae4..a3e948d96 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -30,8 +30,9 @@ val declare_instance_constant :
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
   Id.t -> (** name *)
+  Id.t Loc.located list option ->
   bool -> (* polymorphic *)
-  Univ.universe_context_set -> (* Universes *)
+  Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
   Term.types -> (** type *)
   Names.Id.t
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4adb66bc9..18b2b1444 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -176,7 +176,9 @@ let _ = Obligations.declare_definition_ref :=
        (fun i k c imps hook -> declare_definition i k c [] imps hook)
 
 let do_definition ident k pl bl red_option c ctypopt hook =
-  let (ce, evd, pl, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in
+  let (ce, evd, pl', imps as def) =
+    interp_definition pl bl (pi2 k) red_option c ctypopt
+  in
     if Flags.is_program_mode () then
       let env = Global.env () in
       let (c,ctx), sideff = Future.force ce.const_entry_body in
@@ -193,9 +195,9 @@ let do_definition ident k pl bl red_option c ctypopt hook =
       let ctx = Evd.evar_universe_context evd in
       let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
 	ignore(Obligations.add_definition
-          ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
+          ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ident k ce pl imps
+      ignore(declare_definition ident k ce pl' imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -904,10 +906,11 @@ let nf_evar_context sigma ctx =
   List.map (fun (n, b, t) ->
     (n, Option.map (Evarutil.nf_evar sigma) b, Evarutil.nf_evar sigma t)) ctx
 
-let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
+let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
-  let evdref = ref (Evd.from_env env) in
+  let ctx = Evd.make_evar_universe_context env pl in
+  let evdref = ref (Evd.from_ctx ctx) in
   let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
@@ -1013,9 +1016,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
       let hook l gr _ = 
 	let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
-	let pl, univs = Evd.universe_context !evdref in
+	let pl, univs = Evd.universe_context ?names:pl !evdref in
 	  (*FIXME poly? *)
-	let ce = definition_entry ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
+	let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
 	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
@@ -1039,7 +1042,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
   in
   let ctx = Evd.evar_universe_context !evdref in
-    ignore(Obligations.add_definition recname ~term:evars_def 
+    ignore(Obligations.add_definition recname ~term:evars_def ?pl
 	     evars_typ ctx evars ~hook)
 
 let interp_recursive isfix fixl notations =
@@ -1260,22 +1263,22 @@ let do_program_recursive local p fixkind fixl ntns =
   | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
   | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
   in
-  Obligations.add_mutual_definitions defs ~kind ctx ntns fixkind
+  Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind
 
 let do_program_fixpoint local poly l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
-    | [(n, CWfRec r)], [((((_,id),_),_,bl,typ,def),ntn)] ->
+    | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] ->
 	let recarg = 
 	  match n with
 	  | Some n -> mkIdentC (snd n)
 	  | None ->
 	      errorlabstrm "do_program_fixpoint"
 		(str "Recursive argument required for well-founded fixpoints")
-	in build_wellfounded (id, n, bl, typ, out_def def) r recarg ntn
+	in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
 	     
-    | [(n, CMeasureRec (m, r))], [((((_,id),_),_,bl,typ,def),ntn)] ->
-	build_wellfounded (id, n, bl, typ, out_def def)
+    | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] ->
+	build_wellfounded (id, pl, n, bl, typ, out_def def) poly
 	  (Option.default (CRef (lt_ref,None)) r) m ntn
 	  
     | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8f56cddfa..f46b90111 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -35,7 +35,7 @@ let print_header () =
   ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   pp_flush ()
 
-let warning s = msg_warning (strbrk s)
+let warning s = with_option Flags.warn msg_warning (strbrk s)
 
 let toploop = ref None
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 819c290af..4a5f14917 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -890,7 +890,17 @@ let explain_is_a_functor () =
   str "Illegal use of a functor."
 
 let explain_incompatible_module_types mexpr1 mexpr2 =
-  str "Incompatible module types."
+  let open Declarations in
+  let rec get_arg = function
+  | NoFunctor _ -> 0
+  | MoreFunctor (_, _, ty) -> succ (get_arg ty)
+  in
+  let len1 = get_arg mexpr1.mod_type in
+  let len2 = get_arg mexpr2.mod_type in
+  if len1 <> len2 then
+    str "Incompatible module types: module expects " ++ int len2 ++
+      str " arguments, found " ++ int len1 ++ str "."
+  else str "Incompatible module types."
 
 let explain_not_equal_module_paths mp1 mp2 =
   str "Non equal modules."
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6534c39a7..5a47fc0ea 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -537,10 +537,15 @@ let add_break_if_none n = function
   | l -> UnpCut (PpBrk(n,0)) :: l
 
 let check_open_binder isopen sl m =
+  let pr_token = function
+  | Terminal s -> str s
+  | Break n -> str "␣"
+  | _ -> assert false
+  in
   if isopen && not (List.is_empty sl) then
     errorlabstrm "" (str "as " ++ pr_id m ++
       str " is a non-closed binder, no such \"" ++
-      prlist_with_sep spc (function Terminal s -> str s | _ -> assert false) sl
+      prlist_with_sep spc pr_token sl
       ++ strbrk "\" is allowed to occur.")
 
 (* Heuristics for building default printing rules *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index fd91cfb5c..0ea9f959f 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -299,6 +299,7 @@ type program_info_aux = {
   prg_body: constr;
   prg_type: constr;
   prg_ctx:  Evd.evar_universe_context;
+  prg_pl: Id.t Loc.located list option;
   prg_obligations: obligations;
   prg_deps : Id.t list;
   prg_fixkind : fixpoint_kind option ;
@@ -498,15 +499,21 @@ let declare_definition prg =
     (Evd.evar_universe_context_subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
   let fix_exn = Stm.get_fix_exn () in
+  let pl, ctx =
+    Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
   let ce =
     definition_entry ~fix_exn
      ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
      ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
-    progmap_remove prg;
+  let () = progmap_remove prg in
+  let cst =
     !declare_definition_ref prg.prg_name 
-      prg.prg_kind ce prg.prg_implicits
-      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
+     prg.prg_kind ce prg.prg_implicits
+     (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
+  in
+  Universes.register_universe_binders cst pl;
+  cst
       
 open Pp
 
@@ -634,7 +641,8 @@ let declare_obligation prg obl body ty uctx =
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
 
-let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls impls kind reduce hook =
+let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
+		   notations obls impls kind reduce hook =
   let obls', b = 
     match b with
     | None ->
@@ -654,7 +662,7 @@ let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls
 	  obls, b
   in
     { prg_name = n ; prg_body = b; prg_type = reduce t; 
-      prg_ctx = ctx; 
+      prg_ctx = ctx; prg_pl = pl;
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
@@ -1016,11 +1024,11 @@ let show_term n =
 	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
-let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
     ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
   let sign = Decls.initialize_named_context_for_proof () in
   let info = Id.print n ++ str " has type-checked" in
-  let prg = init_prog_info sign ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
+  let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose msg_info (info ++ str ".");
@@ -1035,13 +1043,13 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
     ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
   let sign = Decls.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info sign ~opaque n (Some b) t ctx deps (Some fixkind)
+     let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
      in progmap_add n (Ephemeron.create prg)) l;
     let _defined =
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index b2320a578..e257da016 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -64,6 +64,7 @@ val get_proofs_transparency : unit -> bool
 
 val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> 
   Evd.evar_universe_context ->
+  ?pl:(Id.t Loc.located list) -> (* Universe binders *)
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
@@ -81,6 +82,7 @@ val add_mutual_definitions :
   (Names.Id.t * Term.constr * Term.types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   Evd.evar_universe_context ->
+  ?pl:(Id.t Loc.located list) -> (* Universe binders *)
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->