From aa1913411547eeed464b024f1cf54113be26e929 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 21 Jan 2016 22:17:36 +0100
Subject: Compile OS X binaries without native_compute support.

---
 dev/make-macos-dmg.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
 
-- 
cgit v1.2.3


From f65f8d5a4d9ba437fa2d8af03e2781d841e53007 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 21 Jan 2016 09:21:23 +0100
Subject: Restore warnings produced by the interpretation of the command line
 (e.g. with deprecated options such as -byte, etc.) since I guess this is what
 we expect.

Was probably lost in 81eb133d64ac81cb.
---
 lib/flags.mli      | 1 +
 toplevel/coqtop.ml | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/lib/flags.mli b/lib/flags.mli
index ab06eda30..69caad5b6 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/toplevel/coqtop.ml b/toplevel/coqtop.ml
index afd4ef40e..cfedff080 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
 
-- 
cgit v1.2.3


From ccdc62a6b4722c38f2b37cbf21b14e5094255390 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 21 Jan 2016 18:05:55 -0500
Subject: Fix bug #4506. Using betadeltaiota_nolet might produce terms of the
 form (let x := t in u) a that should be reduced. Maybe a different
 decomposition/reduction primitive should be used instead.

---
 pretyping/indrec.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index d5f6e9b30..0588dcc87 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -155,7 +155,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 (_,_) ->
@@ -166,7 +166,10 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
                 base [|applist (mkRel (i+1), Termops.extended_rel_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
@@ -230,14 +233,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), Termops.extended_rel_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
-- 
cgit v1.2.3


From 5cbcc8fd761df0779f6202fef935f07cfef8a228 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Sat, 23 Jan 2016 15:17:29 -0500
Subject: Implement support for universe binder lists in Instance and Program
 Fixpoint/Definition.

---
 interp/dumpglob.ml       |  2 +-
 intf/constrexpr.mli      |  2 +-
 parsing/g_vernac.ml4     |  8 ++++----
 parsing/pcoq.ml4         |  1 +
 parsing/pcoq.mli         |  1 +
 printing/ppvernac.ml     |  5 +++--
 tactics/rewrite.ml       |  4 ++--
 toplevel/classes.ml      | 29 +++++++++++++++++------------
 toplevel/classes.mli     |  3 ++-
 toplevel/command.ml      | 29 ++++++++++++++++-------------
 toplevel/obligations.ml  | 26 +++++++++++++++++---------
 toplevel/obligations.mli |  2 ++
 12 files changed, 67 insertions(+), 45 deletions(-)

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 dcdbd47f6..a53238dfd 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -121,7 +121,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/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 839f768b9..f3766a7d7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -192,7 +192,7 @@ let test_plurial_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, ... *)
@@ -783,10 +783,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.ml4 b/parsing/pcoq.ml4
index 32dbeaa4d..28dc74e81 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -315,6 +315,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 24b58775a..54e642387 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -163,6 +163,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/printing/ppvernac.ml b/printing/ppvernac.ml
index d2f59e7b8..38add9d2c 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -925,8 +925,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/rewrite.ml b/tactics/rewrite.ml
index 74bb6d597..83742bfbd 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1703,7 +1703,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))
 
@@ -1919,7 +1919,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/toplevel/classes.ml b/toplevel/classes.ml
index 3a0b5f24f..f73dd5a2e 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -101,19 +101,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
 
@@ -121,7 +123,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 ->
@@ -158,7 +162,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
@@ -185,11 +189,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 =
@@ -282,9 +288,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
@@ -304,7 +309,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 24c51b31a..d600b3104 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -31,8 +31,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 5d2a7638a..8f7c38997 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -177,7 +177,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
@@ -194,9 +196,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)))
 
@@ -905,10 +907,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
@@ -1014,9 +1017,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
@@ -1040,7 +1043,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 =
@@ -1261,22 +1264,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/obligations.ml b/toplevel/obligations.ml
index 314789ced..7e0d30a63 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -311,6 +311,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 ;
@@ -510,15 +511,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
 
@@ -644,7 +651,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 ->
@@ -664,7 +672,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; 
@@ -995,11 +1003,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 = str (Id.to_string 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 ".");
@@ -1014,13 +1022,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) ->
-- 
cgit v1.2.3


From 6a046f8d3e33701d70e2a391741e65564cc0554d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Sat, 23 Jan 2016 15:55:43 -0500
Subject: Fix bug #4519: oops, global shadowed local universe level bindings.

---
 pretyping/pretyping.ml        | 10 +++++-----
 test-suite/bugs/closed/4519.v | 21 +++++++++++++++++++++
 2 files changed, 26 insertions(+), 5 deletions(-)
 create mode 100644 test-suite/bugs/closed/4519.v

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ac0104d9f..b33084a42 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -138,12 +138,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/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
-- 
cgit v1.2.3


From b582db2ecbb3f7f1315fedc50b0009f62f5c59ad Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Sat, 23 Jan 2016 17:28:34 -0500
Subject: Fix bug #4503: mixing universe polymorphic and monomorphic variables
 and definitions in sections is unsupported.

---
 library/declare.ml                    |  4 ++--
 library/lib.ml                        | 22 ++++++++++++++-------
 library/lib.mli                       |  5 +++--
 test-suite/bugs/closed/4503.v         | 37 +++++++++++++++++++++++++++++++++++
 test-suite/bugs/closed/HoTT_coq_002.v |  2 +-
 test-suite/bugs/closed/HoTT_coq_020.v |  4 ++--
 theories/Logic/Hurkens.v              |  3 ++-
 7 files changed, 62 insertions(+), 15 deletions(-)
 create mode 100644 test-suite/bugs/closed/4503.v

diff --git a/library/declare.ml b/library/declare.ml
index 5f6f0fe45..c9d5fdbe2 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 29fc7cd24..513c48549 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_context -> unit
-val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit
+val add_section_kn : Decl_kinds.polymorphic ->
+  Names.mutual_inductive -> Context.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)
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/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.
-- 
cgit v1.2.3


From 4b1103dc38754917e12bf04feca446e02cf55f07 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 24 Jan 2016 12:17:21 +0100
Subject: Fixing bug #4511: evar tactic can create non-typed evars.

---
 tactics/evar_tactics.ml       | 3 +++
 test-suite/bugs/closed/4511.v | 3 +++
 2 files changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/4511.v

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 202aca0de..2887fc228 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -71,6 +71,9 @@ let let_evar name typ =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma 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 in
     let id = match name with
     | Names.Anonymous -> 
       let id = Namegen.id_of_name_using_hdchar env typ name in
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.
+
-- 
cgit v1.2.3


From cb30837323aa462df24ad6668790f67b9bf20b5d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 24 Jan 2016 12:35:49 +0100
Subject: Fixing bug #4495: Failed assertion in metasyntax.ml.

We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
---
 test-suite/bugs/closed/4495.v | 1 +
 toplevel/metasyntax.ml        | 7 ++++++-
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4495.v

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/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ae82b64e8..231b22e25 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -540,10 +540,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 *)
-- 
cgit v1.2.3


From e7852396a452f446135183ec3e1743b731d781c0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 24 Jan 2016 14:18:40 +0100
Subject: Adding a test for bug #4378.

---
 test-suite/bugs/closed/4378.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/4378.v

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.
-- 
cgit v1.2.3


From 030ef2f015e5c592ea7599f0f98a715873c1e4d0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 24 Jan 2016 15:15:16 +0100
Subject: Fixing bug #3826: "Incompatible module types" is uninformative.

---
 toplevel/himsg.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 7ddfd46cd..89c33cb6f 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."
-- 
cgit v1.2.3


From f17096fa9eff103f40e6d381ebeb4313002fa378 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 24 Jan 2016 16:25:38 +0100
Subject: Fixing bug #4373: coqdep does not know about .vio files.

---
 tools/coqdep_common.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 58c8e884c..a90264e26 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -504,15 +504,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
@@ -521,7 +521,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
-- 
cgit v1.2.3


From 5361b02a96704a226b713b6040b67ca01de808fa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 24 Jan 2016 18:00:34 +0100
Subject: Tentative fix for bug #4522: Incorrect "Warning..." on windows.

---
 tools/coq_makefile.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 478cf8875..c4b761827 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
-- 
cgit v1.2.3


From 40cc1067dc5353d43ea2f6643cd8ca954e3e8afa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 26 Jan 2016 17:22:08 +0100
Subject: Fixing bde12b70 about reporting ill-formed constructor.

For instance, in

Inductive I : nat -> nat -> Prop := C : forall z, let '(x,y) := z in  x + y = 0.

the computation of the number of arguments to I was made wrong in bde12b70.
---
 kernel/indtypes.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index f9c2a7b0d..49e858315 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -336,7 +336,7 @@ let typecheck_inductive env mie =
 type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
-  | LocalNotConstructor of rel_context * constr list
+  | LocalNotConstructor of rel_context * int
   | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
@@ -355,11 +355,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 = rel_context_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))))
@@ -548,7 +547,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)
-- 
cgit v1.2.3


From 22a2cc1897f0d9f568ebfb807673e84f6ada491a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 27 Jan 2016 09:36:47 +0100
Subject: Fix bug #4537: Coq 8.5 is slower in typeclass resolution.

The performance enhancement introduced by a895b2c0 for non-polymorphic hints
was actually causing a huge regression in the polymorphic case (and was marked
as such). We fix this by only substituting the metas from the evarmap instead
of the whole evarmap.
---
 pretyping/evd.ml  |  4 ++++
 pretyping/evd.mli |  1 +
 tactics/auto.ml   | 13 ++++++++-----
 3 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 01083142b..544114518 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1467,6 +1467,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/pretyping/evd.mli b/pretyping/evd.mli
index 0b4f18536..9cfca02ed 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -455,6 +455,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/tactics/auto.ml b/tactics/auto.ml
index 2d92387c0..647ff9714 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -85,11 +85,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
-- 
cgit v1.2.3