From 4de7d7fb63a68b766126ae467be1e9bc00b92948 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 9 Jun 2016 19:10:55 +0200
Subject: Reporting about a few bug fixes (to be continued).

---
 CHANGES | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 6a1f8f0e49..dada2ed975 100644
--- a/CHANGES
+++ b/CHANGES
@@ -3,8 +3,12 @@ Changes from V8.5pl1 to V8.5pl2
 
 Bugfixes
 
-- #4677: fix alpha-conversion in notations needing eta-expansion
+- #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
+- #4752: CoqIDE crash on files not ended by ".v".
+- #4398: type_scope used consistently in "match goal".
 
 Changes from V8.5 to V8.5pl1
 ============================
-- 
cgit v1.2.3


From d095d43f09162f3365392f91ebdd48fcf83d9147 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 Jun 2016 08:30:07 +0200
Subject: Fixing a try with in apply that has become too weak in 8.5.

Don't know however what should be the right guard to this try. Now
using catchable_exception, but even in 8.4, Failure was caught, which
is strange.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4562e25184..b1df1f5aa4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1501,7 +1501,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
         if n<0 then error "Applied theorem has not enough premisses.";
         let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
         Clenvtac.res_pf clause ~with_evars ~flags
-      with UserError _ as exn ->
+      with exn when catchable_exception exn ->
         Proofview.tclZERO exn
     in
     let rec try_red_apply thm_ty (exn0, info) =
-- 
cgit v1.2.3


From f9695eb4bc5b377a02f49ee485d7fe9be122c183 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 Jun 2016 07:36:46 +0200
Subject: Fixing #4782 (a typing error not captured when dealing with
 bindings).

Trying to now catch all unification errors, but without a clear view
at whether some errors could be tolerated at the point of checking the
type of the binding.
---
 proofs/clenv.ml               | 2 +-
 test-suite/bugs/closed/4782.v | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4782.v

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 88e1bce95a..09e77602df 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -459,7 +459,7 @@ let clenv_unify_binding_type clenv c t u =
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
     with 
-      | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e ->
+      | PretypeError (_,_,ActualTypeNotCoercible _) as e ->
 	  raise e
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
new file mode 100644
index 0000000000..4622b18d28
--- /dev/null
+++ b/test-suite/bugs/closed/4782.v
@@ -0,0 +1,8 @@
+(* About typing of with bindings *)
+
+Record r : Type := mk_r { type : Type; cond : type -> Prop }.
+
+Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
+
+Goal p.
+Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
-- 
cgit v1.2.3


From 78102fedf6b1dca94cf2695bb1ba2000d4f76db9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 Jun 2016 15:08:16 +0200
Subject: Fixing bug in printing CannotSolveConstraint (collision of context
 names).

---
 toplevel/himsg.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 3ff2d3fb18..fa47cc4311 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -67,10 +67,10 @@ let rec contract3' env a b c = function
   | NotSameArgSize | NotSameHead | NoCanonicalStructure
   | MetaOccurInBody _ | InstanceNotSameType _
   | UnifUnivInconsistency _ as x -> contract3 env a b c, x
-  | CannotSolveConstraint ((pb,env,t,u),x) ->
-      let env,t,u = contract2 env t u in
+  | CannotSolveConstraint ((pb,env',t,u),x) ->
+      let env',t,u = contract2 env' t u in
       let y,x = contract3' env a b c x in
-      y,CannotSolveConstraint ((pb,env,t,u),x)
+      y,CannotSolveConstraint ((pb,env',t,u),x)
 
 (** Printers *)
 
-- 
cgit v1.2.3


From 59e1618ccda6bbc9c627df93db7aaa3ea5930ccf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Jun 2016 15:56:06 +0200
Subject: Protecting eta-expansion in evarconv.ml against ill-typed problems.

This can happen with the "with" clause (see e.g. #4782), but also with
recursive calls in first-order unification (e.g. "?n a a b = f a" when
a matching between "b" and "a" is tried before expanding f).
---
 pretyping/evarconv.ml | 36 +++++++++++++++++++++---------------
 1 file changed, 21 insertions(+), 15 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cc202d73c5..a39e374447 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -462,10 +462,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
   let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
     let switch f a b = if on_left then f a b else f b a in
     let eta evd =
-             match kind_of_term termR with
-	     | Lambda _ -> eta env evd false skR termR skF termF
-	     | Construct u -> eta_constructor ts env evd skR u skF termF
-	     | _ -> UnifFailure (evd,NotSameHead)
+      match kind_of_term termR with
+      | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
+         eta env evd false skR termR skF termF
+      | Construct u -> eta_constructor ts env evd skR u skF termF
+      | _ -> UnifFailure (evd,NotSameHead)
     in
     match Stack.list_of_app_stack skF with
     | None ->
@@ -741,10 +742,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  ise_try evd [f3; f4]
 
     (* Eta-expansion *)
-    | Rigid, _ when isLambda term1 ->
+    | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
         eta env evd true sk1 term1 sk2 term2
 
-    | _, Rigid when isLambda term2 ->
+    | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
         eta env evd false sk2 term2 sk1 term1
 
     | Rigid, Rigid -> begin
@@ -1094,7 +1095,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   abstract_free_holes evd subst, true
   with TypingFailed evd -> evd, false
 
-let second_order_matching_with_args ts env evd ev l t =
+let second_order_matching_with_args ts env evd pbty ev l t =
 (*
   let evd,ev = evar_absorb_arguments env evd ev l in
   let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in
@@ -1102,8 +1103,9 @@ let second_order_matching_with_args ts env evd ev l t =
   if b then Success evd
   else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
   if b then Success evd else
-*)
-  UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
+ *)
+  let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
+  UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
 
 let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
@@ -1119,7 +1121,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
          type inference *)
       (match choose_less_dependent_instance evk1 evd term2 args1 with
       | Some evd -> Success evd
-      | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
+      | None ->
+         let reason = ProblemBeyondCapabilities in
+         UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
   | (Rel _|Var _), Evar (evk2,args2) when app_empty
       && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a)
         (remove_instance_local_defs evd evk2 args2) ->
@@ -1127,7 +1131,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
          type inference *)
       (match choose_less_dependent_instance evk2 evd term1 args2 with
       | Some evd -> Success evd
-      | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
+      | None ->
+         let reason = ProblemBeyondCapabilities in
+         UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
   | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
       let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in
       Success (solve_refl ~can_drop:true f env evd
@@ -1142,20 +1148,20 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       ise_try evd
         [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2);
          (fun evd ->
-           second_order_matching_with_args ts env evd ev1 l1 t2)]
+           second_order_matching_with_args ts env evd pbty ev1 l1 t2)]
   | _,Evar ev2 when Array.length l2 <= Array.length l1 ->
       (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
       (* and otherwise second-order matching *)
       ise_try evd
         [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1);
          (fun evd ->
-           second_order_matching_with_args ts env evd ev2 l2 t1)]
+           second_order_matching_with_args ts env evd pbty ev2 l2 t1)]
   | Evar ev1,_ ->
       (* Try second-order pattern-matching *)
-      second_order_matching_with_args ts env evd ev1 l1 t2
+      second_order_matching_with_args ts env evd pbty ev1 l1 t2
   | _,Evar ev2 ->
       (* Try second-order pattern-matching *)
-      second_order_matching_with_args ts env evd ev2 l2 t1
+      second_order_matching_with_args ts env evd pbty ev2 l2 t1
   | _ ->
       (* Some head evar have been instantiated, or unknown kind of problem *)
       evar_conv_x ts env evd pbty t1 t2
-- 
cgit v1.2.3


From 1f772656fa4bb6899ffea84ad5483e9690bbdc08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Jun 2016 16:00:23 +0200
Subject: Reserve exception "ConversionFailed" in unification for failure of
 conversion on closed terms.

This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
---
 pretyping/pretype_errors.ml  | 5 +++--
 pretyping/pretype_errors.mli | 1 +
 toplevel/himsg.ml            | 4 +++-
 3 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index cf5b08c58f..b0715af734 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -14,15 +14,16 @@ open Type_errors
 
 type unification_error =
   | OccurCheck of existential_key * constr
-  | NotClean of existential * env * constr
+  | NotClean of existential * env * constr (* Constr is a variable not in scope *)
   | NotSameArgSize
   | NotSameHead
   | NoCanonicalStructure
-  | ConversionFailed of env * constr * constr
+  | ConversionFailed of env * constr * constr (* Non convertible closed terms *)
   | MetaOccurInBody of existential_key
   | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
   | CannotSolveConstraint of Evd.evar_constraint * unification_error
+  | ProblemBeyondCapabilities
 
 type position = (Id.t * Locus.hyp_location_flag) option
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index f617df9ee7..880f48e5f9 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -24,6 +24,7 @@ type unification_error =
   | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
   | CannotSolveConstraint of Evd.evar_constraint * unification_error
+  | ProblemBeyondCapabilities
 
 type position = (Id.t * Locus.hyp_location_flag) option
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index fa47cc4311..244174f651 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -65,7 +65,7 @@ let rec contract3' env a b c = function
       let (env',t1,t2) = contract2 env' t1 t2 in
       contract3 env a b c, ConversionFailed (env',t1,t2)
   | NotSameArgSize | NotSameHead | NoCanonicalStructure
-  | MetaOccurInBody _ | InstanceNotSameType _
+  | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities
   | UnifUnivInconsistency _ as x -> contract3 env a b c, x
   | CannotSolveConstraint ((pb,env',t,u),x) ->
       let env',t,u = contract2 env' t u in
@@ -310,6 +310,8 @@ let rec explain_unification_error env sigma p1 p2 = function
         (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++
         str " == " ++ pr_lconstr_env env sigma u)
         :: aux t u e
+     | ProblemBeyondCapabilities ->
+        []
      in
      match aux p1 p2 e with
      | [] -> mt ()
-- 
cgit v1.2.3


From 827663982e9cdf502f21727677515cf2318aa41d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Jun 2016 14:53:38 +0200
Subject: Another fix to #4782 (a typing error not captured when dealing with
 bindings).

The tentative fix in f9695eb4b (which I was afraid it might be too
strong, since it was implying failing more often) indeed broke other
things (see #4813).
---
 proofs/clenv.ml               | 3 ++-
 test-suite/bugs/closed/4782.v | 1 +
 test-suite/bugs/closed/4813.v | 9 +++++++++
 3 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4813.v

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 09e77602df..79b331a273 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -459,7 +459,8 @@ let clenv_unify_binding_type clenv c t u =
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
     with 
-      | PretypeError (_,_,ActualTypeNotCoercible _) as e ->
+      | PretypeError (_,_,ActualTypeNotCoercible (_,_,
+          (NotClean _ | ConversionFailed _))) as e ->
 	  raise e
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
index 4622b18d28..ed44437861 100644
--- a/test-suite/bugs/closed/4782.v
+++ b/test-suite/bugs/closed/4782.v
@@ -6,3 +6,4 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
 
 Goal p.
 Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
+ 
diff --git a/test-suite/bugs/closed/4813.v b/test-suite/bugs/closed/4813.v
new file mode 100644
index 0000000000..5f8ea74c1a
--- /dev/null
+++ b/test-suite/bugs/closed/4813.v
@@ -0,0 +1,9 @@
+(* On the strength of "apply with" (see also #4782) *)
+
+Record ProverT := { Facts : Type }.
+Record ProverT_correct (P : ProverT) :=  { Valid : Facts P -> Prop ;
+                                           Valid_weaken : Valid = Valid }.
+Definition reflexivityValid (_ : unit) := True.
+Definition reflexivityProver_correct : ProverT_correct {| Facts := unit |}.
+Proof.
+    eapply Build_ProverT_correct with (Valid := reflexivityValid).
-- 
cgit v1.2.3


From 19aa7231ec96dbbfdda7788679cf7ddf00bda7a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Jun 2016 16:06:43 +0200
Subject: Minor simplification in evarconv.

Function default_fail was always part of an ise_try. Its associated
error message was anyway thrown away. It is then irrelevant and could
be made simpler.
---
 pretyping/evarconv.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a39e374447..96c90e2fc0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -362,8 +362,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
 
 and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
-  let default_fail i = (* costly *)
-    UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in
   let quick_fail i = (* not costly, loses info *)
     UnifFailure (i, NotSameHead)
   in
@@ -415,7 +413,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let not_only_app = Stack.not_purely_applicative skM in
     let f1 i =
       match Stack.list_of_app_stack skF with
-      | None -> default_fail evd
+      | None -> quick_fail evd
       | Some lF -> 
         let tM = Stack.zip apprM in
 	  miller_pfenning on_left
-- 
cgit v1.2.3


From 87be9070b3415f31027b78165b213de34c168043 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 13 Jun 2016 11:27:22 +0200
Subject: Tentatively fixing misguiding error message with "binder" type in
 non-recursive notations (#4815).

---
 toplevel/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 2ccd27acb9..92208e3046 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -982,7 +982,7 @@ let make_interpretation_type isrec = function
   | NtnInternTypeConstr when isrec -> NtnTypeConstrList
   | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr
   | NtnInternTypeBinder when isrec -> NtnTypeBinderList
-  | NtnInternTypeBinder -> error "Type not allowed in recursive notation."
+   | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders."
 
 let make_interpretation_vars recvars allvars =
   let eq_subscope (sc1, l1) (sc2, l2) =
-- 
cgit v1.2.3


From bb43103f7ecea16e634d448215f24d6d55d56eb1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 13 Jun 2016 16:37:29 +0200
Subject: evar_conv: Refine occur_rigidly

This avoids postponing constraints which will surely produce
an occur-check and allow to backtrack on first-order unifications
producing those constraints directly (e.g. to apply eta).
(fixes HoTT/HoTT with 8.5).
---
 pretyping/evarconv.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 96c90e2fc0..aead1cb35f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -97,8 +97,7 @@ let position_problem l2r = function
   | CUMUL -> Some l2r
 
 let occur_rigidly ev evd t = 
-  let (l, app) = decompose_app_vect t in 
-  let rec aux t = 
+  let rec aux t =
     match kind_of_term (whd_evar evd t) with
     | App (f, c) -> if aux f then Array.exists aux c else false
     | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
@@ -110,7 +109,7 @@ let occur_rigidly ev evd t =
     | Prod (_, b, t) -> ignore(aux b || aux t); true
     | Rel _ | Var _ -> false
     | Case _ -> false
-  in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app
+  in try ignore(aux t); false with Occur -> true
 
 (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose 
    the problem (t1 stack1) = (t2 stack2) into a problem
-- 
cgit v1.2.3