Merge branch 'v8.5'

10 files changed, 61 insertions, 31 deletions

diff --git a/CHANGES b/CHANGES
index 41d61ec459..82076168ac 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,8 +36,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
 ============================
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 7ec7d21c0c..e5fc5a188d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -103,8 +103,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
@@ -116,7 +115,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
@@ -368,8 +367,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
@@ -421,7 +418,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
@@ -468,10 +465,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 ->
@@ -747,10 +745,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
@@ -1106,7 +1104,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
@@ -1114,8 +1112,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
@@ -1131,7 +1130,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) ->
@@ -1139,7 +1140,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_fconv ~reds:ts pbty env evd x y in
       Success (solve_refl ~can_drop:true f env evd
@@ -1154,20 +1157,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
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/proofs/clenv.ml b/proofs/clenv.ml
index 1ef0b087ba..78dce0d64c 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -491,7 +491,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 (_,_,NotClean _)) as e ->
+      | PretypeError (_,_,ActualTypeNotCoercible (_,_,
+          (NotClean _ | ConversionFailed _))) as e ->
 	  raise e
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 858cc482ae..991922d909 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1661,7 +1661,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) =
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
new file mode 100644
index 0000000000..ed44437861
--- /dev/null
+++ b/test-suite/bugs/closed/4782.v
@@ -0,0 +1,9 @@
+(* 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.
+ 
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).
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ad848ccfc8..e17cd20863 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -69,12 +69,12 @@ 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
+  | 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)
 
 (** Ad-hoc reductions *)
 
@@ -323,6 +323,8 @@ let 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 ()
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 52117f13f6..b22d53f546 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -827,7 +827,7 @@ let make_interpretation_type isrec isonlybinding = function
   | NtnInternTypeConstr | NtnInternTypeIdent ->
      if isonlybinding then NtnTypeOnlyBinder else 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) =