From b4069d5c9933ab645700b511fe8c101e1e16ff48 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 21:21:30 +0200
Subject: Forbidding silently dropped universes instances in  internalization.

Patch by PMP, test-suite fix by MS.
---
 interp/constrintern.ml            | 24 +++++++++++++++---------
 test-suite/bugs/closed/4375.v     |  9 +++++----
 test-suite/success/vm_univ_poly.v | 12 ++++++------
 3 files changed, 26 insertions(+), 19 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ead68bd92f..b6fce61781 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -656,7 +656,13 @@ let string_of_ty = function
   | Method -> "meth"
   | Variable -> "var"
 
-let intern_var genv (ltacvars,ntnvars) namedctx loc id =
+let gvar (loc, id) us = match us with
+| None -> GVar (loc, id)
+| Some _ ->
+  user_err_loc (loc, "", str "Variable " ++ pr_id id ++
+    str " cannot have a universe instance")
+
+let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   (* Is [id] an inductive type potentially with implicit *)
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
@@ -664,21 +670,21 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
       (fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
-    GVar (loc,id), make_implicits_list impls, argsc, expl_impls
+    gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
   if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars
   then
-    GVar (loc,id), [], [], []
+    gvar (loc,id) us, [], [], []
   (* Is [id] a notation variable *)
   else if Id.Map.mem id ntnvars
   then
-    (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
+    (set_var_scope loc id true genv ntnvars; gvar (loc,id) us, [], [], [])
   (* Is [id] the special variable for recursive notations *)
   else if Id.equal id ldots_var
   then if Id.Map.is_empty ntnvars
     then error_ldots_var loc
-    else GVar (loc,id), [], [], []
+    else gvar (loc,id) us, [], [], []
   else if Id.Set.mem id ltacvars.ltac_bound then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
     user_err_loc (loc,"intern_var",
@@ -693,10 +699,10 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
 	let impls = implicits_of_global ref in
 	let scopes = find_arguments_scope ref in
 	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
-	GRef (loc, ref, None), impls, scopes, []
+	GRef (loc, ref, us), impls, scopes, []
       with e when Errors.noncritical e ->
 	(* [id] a goal variable *)
-	GVar (loc,id), [], [], []
+	gvar (loc,id) us, [], [], []
 
 let proj_impls r impls =
   let env = Global.env () in
@@ -792,7 +798,7 @@ let intern_applied_reference intern env namedctx lvar us args = function
       let x, imp, scopes, l = find_appl_head_data r in
 	(x,imp,scopes,l), args2
   | Ident (loc, id) ->
-      try intern_var env lvar namedctx loc id, args
+      try intern_var env lvar namedctx loc id us, args
       with Not_found ->
       let qid = qualid_of_ident id in
       try
@@ -802,7 +808,7 @@ let intern_applied_reference intern env namedctx lvar us args = function
       with Not_found ->
 	(* Extra allowance for non globalizing functions *)
 	if !interning_grammar || env.unb then
-	  (GVar (loc,id), [], [], []), args
+	  (gvar (loc,id) us, [], [], []), args
 	else error_global_not_found_loc loc qid
 
 let interp_reference vars r =
diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v
index 03af16535b..71e3a75187 100644
--- a/test-suite/bugs/closed/4375.v
+++ b/test-suite/bugs/closed/4375.v
@@ -93,14 +93,15 @@ Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} :=
 | A : foo T -> foo T.
 
 Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t :=
-  @A@{i} t (cg@{i} t).
+  @A@{i} t (cg t).
 
 Print cg.
 
 Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t :=
-  @A@{i} t (@cb@{i} t)
+  @A@{i} t (cb t)
 with cb@{i} (t : Type@{i}) : foo@{i} t :=
-  @A@{i} t (@ca@{i} t).
+  @A@{i} t (ca t).
 
 Print ca.
-Print cb.
\ No newline at end of file
+Print cb.
+  
\ No newline at end of file
diff --git a/test-suite/success/vm_univ_poly.v b/test-suite/success/vm_univ_poly.v
index 58fa39743d..62df96c0b8 100644
--- a/test-suite/success/vm_univ_poly.v
+++ b/test-suite/success/vm_univ_poly.v
@@ -38,8 +38,8 @@ Definition _4 : sumbool_copy x = x :=
 
 (* Polymorphic Inductive Types *)
 Polymorphic Inductive poption@{i} (T : Type@{i}) : Type@{i} :=
-| PSome : T -> poption@{i} T
-| PNone : poption@{i} T.
+| PSome : T -> poption T
+| PNone : poption T.
 
 Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T :=
   match p with
@@ -49,7 +49,7 @@ Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x
 
 Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} :=
 | pnil
-| pcons : T -> plist@{i} T -> plist@{i} T.
+| pcons : T -> plist T -> plist T.
 
 Arguments pnil {_}.
 Arguments pcons {_} _ _.
@@ -59,7 +59,7 @@ Polymorphic Definition pmap@{i j}
   fix pmap (ls : plist@{i} T) : plist@{j} U :=
     match ls with
     | @pnil _ => @pnil _
-    | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls)
+    | @pcons _ l ls => @pcons@{j} U (f l) (pmap ls)
     end.
 
 Universe Ubool.
@@ -75,7 +75,7 @@ Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) p
 
 Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} :=
 | Empty
-| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T.
+| Branch : plist@{i} (Tree T) -> Tree T.
 
 Polymorphic Definition pfold@{i u}
             {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) :=
@@ -111,7 +111,7 @@ Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i}
 Polymorphic Fixpoint big_tree@{i} (n : nat@{i}) : Tree@{i} nat@{i} :=
   match n with
   | O => @Empty nat@{i}
-  | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree@{i} n'))
+  | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree n'))
   end.
 
 Eval compute in height (big_tree (S (S (S O)))).
-- 
cgit v1.2.3


From 6863389c13e85d2728c4d3c3ac40b20172e9e98b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 21:21:56 +0200
Subject: Univs: allowing notations to take univ instances

They can apply to the head reference under a notation.
---
 interp/constrintern.ml        | 5 ++++-
 test-suite/bugs/closed/3825.v | 8 ++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b6fce61781..f30d3cefad 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -777,9 +777,12 @@ let intern_qualid loc qid intern env lvar us args =
       let c = match us, c with
       | None, _ -> c
       | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
+      | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
+         GApp (loc, GRef (loc', ref, us), arg)
       | Some _, _ ->
         user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++
-          str " cannot have a universe instance")
+          str " cannot have a universe instance, its expanded head
+               does not start with a reference")
       in
       c, projapp, args2
 
diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
index e594b74b62..666c64631f 100644
--- a/test-suite/bugs/closed/3825.v
+++ b/test-suite/bugs/closed/3825.v
@@ -14,3 +14,11 @@ Notation qux := (nat -> nat).
 
 Fail Check qux@{i}.
 
+Axiom TruncType@{i} : nat -> Type@{i}.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hProp := (0)-Type.
+
+Check hProp.
+Check hProp@{i}.
+
-- 
cgit v1.2.3


From 086346a72b708dd349f367bf7ad5784c26e46d78 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 20 Apr 2016 11:41:24 +0200
Subject: Refine fix for bug #4097, avoid proj expansion

---
 pretyping/evarsolve.ml | 31 +++++++++++++++----------------
 1 file changed, 15 insertions(+), 16 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3bf6f37649..29af199a1e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -208,30 +208,29 @@ let restrict_instance evd evk filter argsv =
 
 let noccur_evar env evd evk c =
   let cache = ref Int.Set.empty (* cache for let-ins *) in
-  let rec occur_rec (k, env as acc) c =
+  let rec occur_rec check_types (k, env as acc) c =
   match kind_of_term c with
   | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
-       | Some c -> occur_rec acc c
+       | Some c -> occur_rec check_types acc c
        | None ->
            if Evar.equal evk evk' then raise Occur
-           else Array.iter (occur_rec acc) args')
+           else (if check_types then
+                   occur_rec false acc (existential_type evd ev');
+                 Array.iter (occur_rec check_types acc) args'))
   | Rel i when i > k ->
-      if not (Int.Set.mem (i-k) !cache) then
-      (match pi2 (Environ.lookup_rel i env) with
-       | None -> ()
-       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b))
-  | Proj (p,c) -> 
-    let c = 
-      try Retyping.expand_projection env evd p c []
-      with Retyping.RetypeError _ -> 
-	(* Can happen when called from w_unify which doesn't assign evars/metas 
-	   eagerly enough *) c
-    in occur_rec acc c
+     if not (Int.Set.mem (i-k) !cache) then
+       let decl = Environ.lookup_rel i env in
+       if check_types then
+         (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (pi3 decl)));
+       (match pi2 decl with
+        | None -> ()
+        | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i b))
+  | Proj (p,c) -> occur_rec true acc c
   | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env))
-    occur_rec acc c
+    (occur_rec check_types) acc c
   in
-  try occur_rec (0,env) c; true with Occur -> false
+  try occur_rec false (0,env) c; true with Occur -> false
 
 (***************************************)
 (* Managing chains of local definitons *)
-- 
cgit v1.2.3


From 11b32aa76f63525bb5bcf1b3171514f6f6830606 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jun 2016 16:29:03 +0200
Subject: Univs/CHANGES: #4097 and annotations on notations

---
 CHANGES | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGES b/CHANGES
index dada2ed975..2533b01897 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,13 @@ Bugfixes
 - #4777: printing inefficiency with implicit arguments
 - #4752: CoqIDE crash on files not ended by ".v".
 - #4398: type_scope used consistently in "match goal".
+- #4097: more efficient occur-check in presence of primitive projections
+
+Universes:
+- Disallow silently dropping universe instances applied to variables
+  (forward compatible)
+- Allow explicit universe instances on notations, when they can apply
+  to the head reference of their expansion.
 
 Changes from V8.5 to V8.5pl1
 ============================
-- 
cgit v1.2.3


From 1cc70be070e1df522b1539892958496a77710331 Mon Sep 17 00:00:00 2001
From: Gabriel Scherer
Date: Tue, 28 Jun 2016 14:45:37 -0400
Subject: fix coqide double module linking (error on OCaml 4.03)

Linking the same module twice in OCaml can have problematic unintended
consequences and lead to hard-to-understand bugs, see
  http://caml.inria.fr/mantis/view.php?id=4231
  http://caml.inria.fr/mantis/view.php?id=5461

OCaml has long warned when double-linking happens

  Warning 31: files FOO and BAR both define a module named Baz

In 4.03 this error was turned into a warning by default.

Coqide does double-linking by passing both
xml_{lexer,parser,printer}.cmo and lib/clib.cma that already contains
these compilation units to bin/coqide.byte. To fix compilation of
Coqide under 4.03, the present patch removes the .cmo from the
command-line arguments.

P.S.: I checked that this patch applies cleanly to the current trunk
(b161ad97fdc01ac8816341a089365657cebc6d2b). It should also be possible
to add it as a patch on top of the 8.5 archives (for example those
distributed through OPAM) to make them compile under 4.03.
---
 Makefile.build  | 2 +-
 Makefile.common | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 0f85608f9a..b5c933a168 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -653,7 +653,7 @@ $(COQWORKMGR): $(addsuffix $(BESTOBJ), stm/coqworkmgrApi tools/coqworkmgr) \
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
+$(FAKEIDE): lib/clib$(BESTLIB) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,-I ide,str unix threads)
 
diff --git a/Makefile.common b/Makefile.common
index 1a903539c2..0dfd5deb7e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -231,7 +231,7 @@ endif
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
-IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo
+IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo
 IDECMA:=ide/ide.cma
 IDETOPLOOPCMA=ide/coqidetop.cma
 
-- 
cgit v1.2.3


From dae240f31d6de1d5b3737d6d0779e009f3d67fa2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 1 Jul 2016 12:48:26 +0200
Subject: Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type
 with evars).

But there are still bugs with Declare Implicit Tactic, which should
probably rather be reimplemented with ltac:(tac).

Indeed, it does support evars in the type of the term, and
solve_by_implicit_tactic should transfer universe constraints to the
main goal. E.g., the following still fails, at Qed time.

Definition Foo {T}{a : T} : T := a.
Declare Implicit Tactic eassumption.
Goal forall A (x : A), A.
intros.
apply Foo.
Qed.
---
 proofs/pfedit.ml              |  4 +++-
 test-suite/bugs/closed/4882.v | 50 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4882.v

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a515c9e750..20cae84a49 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -230,8 +230,10 @@ let solve_by_implicit_tactic env sigma evk =
 	(Environ.named_context env) ->
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
       (try
+        let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
+        if Evarutil.has_undefined_evars sigma c then raise Exit;
         let (ans, _, _) = 
-	  build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in
+	  build_by_tactic env (Evd.evar_universe_context sigma) c tac in
         ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v
new file mode 100644
index 0000000000..8c26af708b
--- /dev/null
+++ b/test-suite/bugs/closed/4882.v
@@ -0,0 +1,50 @@
+
+Definition Foo {T}{a : T} : T := a.
+
+Module A.
+
+  Declare Implicit Tactic eauto.
+
+  Goal forall A (x : A), A.
+  intros.
+  apply Foo. (* Check defined evars are normalized *)
+  (*  Qed. *)
+  Abort.
+
+End A.
+
+Module B.
+
+  Definition Foo {T}{a : T} : T := a.
+
+  Declare Implicit Tactic eassumption.
+
+  Goal forall A (x : A), A.
+  intros.
+  apply Foo.
+  (*  Qed. *)
+  Abort.
+
+End B.
+
+Module C.
+
+  Declare Implicit Tactic first [exact True|assumption].
+
+  Goal forall (x : True), True.
+  intros.
+  apply (@Foo _ _).
+  Qed.
+
+End C.
+
+Module D.
+
+  Declare Implicit Tactic assumption.
+
+  Goal forall A (x : A), A.
+  intros.
+  exact _.
+  Qed.
+
+End D.
-- 
cgit v1.2.3


From 622c663094717530bc767dacce44b39041b9a732 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 1 Jul 2016 13:56:02 +0200
Subject: Fixing #4881 (synchronizing "Declare Implicit Tactic" with
 backtrack).

---
 proofs/pfedit.ml         |  2 +-
 tactics/extratactics.ml4 | 26 ++++++++++++++++++++++----
 2 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 20cae84a49..d3162c54f2 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -215,7 +215,7 @@ let refine_by_tactic env sigma ty tac =
 (* Support for resolution of evars in tactic interpretation, including
    resolution by application of tactics *)
 
-let implicit_tactic = ref None
+let implicit_tactic = Summary.ref None ~name:"implicit-tactic"
 
 let declare_implicit_tactic tac = implicit_tactic := Some tac
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 15613c7ecc..92d0ac983d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -525,11 +525,29 @@ VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF
     [ add_transitivity_lemma false t ]
 END
 
+let cache_implicit_tactic (_,tac) = match tac with
+  | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac)
+  | None -> Pfedit.clear_implicit_tactic ()
+
+let subst_implicit_tactic (subst,tac) =
+  Option.map (Tacsubst.subst_tactic subst) tac
+
+let inImplicitTactic : glob_tactic_expr option -> obj =
+  declare_object {(default_object "IMPLICIT-TACTIC") with
+       open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o);
+       cache_function = cache_implicit_tactic;
+       subst_function = subst_implicit_tactic;
+       classify_function = (fun o -> Dispose)}
+
+let declare_implicit_tactic tac =
+  Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac)))
+
+let clear_implicit_tactic () =
+  Lib.add_anonymous_leaf (inImplicitTactic None)
+
 VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF
-| [ "Declare" "Implicit" "Tactic" tactic(tac) ] ->
-    [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ]
-| [ "Clear" "Implicit" "Tactic" ] ->
-    [ Pfedit.clear_implicit_tactic () ]
+| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ]
+| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ]
 END
 
 
-- 
cgit v1.2.3


From b1a13bc7af4f4b8b5249712d0a982cc510a2cb85 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 1 Jul 2016 15:47:10 +0200
Subject: Fixing use of "Declare Implicit Tactic" in refine.

---
 tactics/extratactics.ml4 | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 92d0ac983d..06fea367af 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -345,11 +345,18 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
+let constr_flags = {
+  Pretyping.use_typeclasses = true;
+  Pretyping.use_unif_heuristics = true;
+  Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+  Pretyping.fail_evar = false;
+  Pretyping.expand_evars = true }
+
 let refine_tac simple {Glob_term.closure=closure;term=term} =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let flags = Pretyping.all_no_fail_flags in
+    let flags = constr_flags in
     let tycon = Pretyping.OfType concl in
     let lvar = { Pretyping.empty_lvar with
       Pretyping.ltac_constrs = closure.Glob_term.typed;
-- 
cgit v1.2.3


From 2ce64cc3124d30dbd42324c345cec378ccd66106 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 4 Jul 2016 09:51:26 +0200
Subject: test-suite: test checking of libraries checksum.

---
 test-suite/Makefile             | 22 +++++++++++++++++++++-
 test-suite/misc/deps/A/A.v      |  1 +
 test-suite/misc/deps/B/A.v      |  1 +
 test-suite/misc/deps/B/B.v      |  7 +++++++
 test-suite/misc/deps/checksum.v |  2 ++
 5 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/misc/deps/A/A.v
 create mode 100644 test-suite/misc/deps/B/A.v
 create mode 100644 test-suite/misc/deps/B/B.v
 create mode 100644 test-suite/misc/deps/checksum.v

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 207f25ed0b..f1cb21ecd5 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -361,7 +361,7 @@ modules/%.vo: modules/%.v
 # Miscellaneous tests
 #######################################################################
 
-misc: misc/deps-order.log misc/universes.log
+misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log
 
 # Check that both coqdep and coqtop/coqc supports -R
 # Check that both coqdep and coqtop/coqc takes the later -R
@@ -390,6 +390,26 @@ misc/deps-order.log:
 	  rm $$tmpoutput; \
 	} > "$@"
 
+deps-checksum: misc/deps-checksum.log
+misc/deps-checksum.log:
+	@echo "TEST      misc/deps-checksum"
+	$(HIDE){ \
+	  echo $(call log_intro,deps-checksum); \
+	  rm -f misc/deps/*/*.vo; \
+	  $(bincoqc) -R misc/deps/A A misc/deps/A/A.v; \
+	  $(bincoqc) -R misc/deps/B A misc/deps/B/A.v; \
+	  $(bincoqc) -R misc/deps/B A misc/deps/B/B.v; \
+	  $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \
+	  if [ $$? = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    misc/deps-checksum...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    misc/deps-checksum...Error!"; \
+	  fi; \
+	} > "$@"
+
+
 # Sort universes for the whole standard library
 EXPECTED_UNIVERSES := 5
 universes: misc/universes.log
diff --git a/test-suite/misc/deps/A/A.v b/test-suite/misc/deps/A/A.v
new file mode 100644
index 0000000000..49aaf4a79e
--- /dev/null
+++ b/test-suite/misc/deps/A/A.v
@@ -0,0 +1 @@
+Definition b := true.
diff --git a/test-suite/misc/deps/B/A.v b/test-suite/misc/deps/B/A.v
new file mode 100644
index 0000000000..c01a30dca5
--- /dev/null
+++ b/test-suite/misc/deps/B/A.v
@@ -0,0 +1 @@
+Definition b := false.
diff --git a/test-suite/misc/deps/B/B.v b/test-suite/misc/deps/B/B.v
new file mode 100644
index 0000000000..f3cda70a9d
--- /dev/null
+++ b/test-suite/misc/deps/B/B.v
@@ -0,0 +1,7 @@
+Require A.
+
+Definition c := A.b.
+Lemma foo : c = false.
+Proof.
+reflexivity.
+Qed.
diff --git a/test-suite/misc/deps/checksum.v b/test-suite/misc/deps/checksum.v
new file mode 100644
index 0000000000..450045e4bf
--- /dev/null
+++ b/test-suite/misc/deps/checksum.v
@@ -0,0 +1,2 @@
+Require Import A.
+Fail Require Import B.
-- 
cgit v1.2.3


From 0eb08b70f0c576e58912c1fc3ef74f387ad465be Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 4 Jul 2016 15:02:48 +0200
Subject: Revert "Improve the interpretation scope of arguments of an ltac
 match."

We apply this patch to trunk for integration in 8.6 instead.

This reverts commit 715f547816addf3e2e9dc288327fcbcee8c6d47f.
---
 tactics/tacintern.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index e60bc459b8..11f2c5943d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -423,7 +423,7 @@ let intern_hyp_location ist ((occs,id),hl) =
 (* Reads a pattern *)
 let intern_pattern ist ?(as_type=false) ltacvars = function
   | Subterm (b,ido,pc) ->
-      let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in
+      let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
       ido, metas, Subterm (b,ido,pc)
   | Term pc ->
       let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
@@ -445,7 +445,7 @@ let opt_cons accu = function
 | Some id -> Id.Set.add id accu
 
 (* Reads the hypotheses of a "match goal" rule *)
-let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
+let rec intern_match_goal_hyps ist lfun = function
   | (Hyp ((_,na) as locna,mp))::tl ->
       let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
       let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
@@ -454,7 +454,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
   | (Def ((_,na) as locna,mv,mp))::tl ->
       let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
       let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
-      let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in
+      let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
       let lfun' = name_cons (opt_cons (opt_cons lfun ido) ido') na in
       lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
   | [] -> lfun, [], []
@@ -600,7 +600,7 @@ and intern_tactic_seq onlytac ist = function
       ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
 
   | TacMatchGoal (lz,lr,lmr) ->
-      ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist ~as_type:true lmr)
+      ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr)
   | TacMatch (lz,c,lmr) ->
       ist.ltacvars,
       TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
@@ -718,18 +718,18 @@ and intern_tacarg strict onlytac ist = function
       anomaly ~loc (str "Unknown dynamic: <" ++ str tag ++ str ">")
 
 (* Reads the rules of a Match Context or a Match *)
-and intern_match_rule onlytac ist ?(as_type=false) = function
+and intern_match_rule onlytac ist = function
   | (All tc)::tl ->
-      All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist ~as_type tl)
+      All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
   | (Pat (rl,mp,tc))::tl ->
       let {ltacvars=lfun; genv=env} = ist in
-      let lfun',metas1,hyps = intern_match_goal_hyps ist ~as_type lfun rl in
-      let ido,metas2,pat = intern_pattern ist ~as_type lfun mp in
+      let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
+      let ido,metas2,pat = intern_pattern ist lfun mp in
       let fold accu x = Id.Set.add x accu in
       let ltacvars = List.fold_left fold (opt_cons lfun' ido) metas1 in
       let ltacvars = List.fold_left fold ltacvars metas2 in
       let ist' = { ist with ltacvars } in
-      Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist ~as_type tl)
+      Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
   | [] -> []
 
 and intern_genarg ist x =
-- 
cgit v1.2.3


From c22f6694bac3479426cf179839430d9d8675e456 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 4 Jul 2016 15:04:30 +0200
Subject: Mention more fixes in CHANGES before we release pl2.

---
 CHANGES | 29 +++++++++++++++++++++++------
 1 file changed, 23 insertions(+), 6 deletions(-)

diff --git a/CHANGES b/CHANGES
index 2533b01897..0f5ea97aa2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,22 +1,39 @@
 Changes from V8.5pl1 to V8.5pl2
 ===============================
 
-Bugfixes
+Critical bugfix
+- Checksums of .vo files dependencies were not correctly checked.
+
+Other bugfixes
 
+- #4097: more efficient occur-check in presence of primitive projections
+- #4398: type_scope used consistently in "match goal".
+- #4450: eauto does not work with polymorphic lemmas
 - #4677: fix alpha-conversion in notations needing eta-expansion.
 - Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode.
 - #4644: a regression in unification.
-- #4777: printing inefficiency with implicit arguments
+- #4725: Function (Error: Conversion test raised an anomaly) and Program
+  (Error: Cannot infer this placeholder of type)
+- #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings
 - #4752: CoqIDE crash on files not ended by ".v".
-- #4398: type_scope used consistently in "match goal".
-- #4097: more efficient occur-check in presence of primitive projections
-
-Universes:
+- #4777: printing inefficiency with implicit arguments
+- #4818: "Admitted" fails due to undefined universe anomaly after calling
+  "destruct"
+- #4823: remote counter: avoid thread race on sockets
+- #4881: synchronizing "Declare Implicit Tactic" with backtrack.
+- #4882: anomaly with Declare Implicit Tactic on hole of type with evars
+- Fix use of "Declare Implicit Tactic" in refine.
+  triggered by CoqIDE
+
+Universes
 - Disallow silently dropping universe instances applied to variables
   (forward compatible)
 - Allow explicit universe instances on notations, when they can apply
   to the head reference of their expansion.
 
+Build infrastructure
+- New update on how to find camlp5 binary and library at configure time.
+
 Changes from V8.5 to V8.5pl1
 ============================
 
-- 
cgit v1.2.3