Merge branch 'v8.6'

4 files changed, 18 insertions, 14 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 077ee4e150..1bd03491a7 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -18,12 +18,12 @@ module NamedDecl = Context.Named.Declaration
 (*i*)
 
 let name_table =
-  Summary.ref (Refmap.empty : Name.t list list Refmap.t)
+  Summary.ref (Refmap.empty : Name.t list Refmap.t)
     ~name:"rename-arguments"
 
 type req =
   | ReqLocal
-  | ReqGlobal of global_reference * Name.t list list
+  | ReqGlobal of global_reference * Name.t list
 
 let load_rename_args _ (_, (_, (r, names))) =
   name_table := Refmap.add r names !name_table
@@ -51,7 +51,7 @@ let discharge_rename_args = function
        let vars,_,_ = section_segment_of_reference c in
        let c' = pop_global_reference c in
        let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
-       let names' = List.map (fun l -> var_names @ l) names in
+       let names' = var_names @ names in
        Some (ReqGlobal (c', names), (c', names'))
      with Not_found -> Some req)
   | _ -> None
@@ -85,7 +85,7 @@ let rec rename_prod c = function
       | _ -> c
         
 let rename_type ty ref =
-  try rename_prod ty (List.hd (arguments_names ref))
+  try rename_prod ty (arguments_names ref)
   with Not_found -> ty
 
 let rename_type_of_constant env c =
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index a334055011..e123e77862 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -11,10 +11,10 @@ open Globnames
 open Environ
 open Term
 
-val rename_arguments : bool -> global_reference -> Name.t list list -> unit
+val rename_arguments : bool -> global_reference -> Name.t list -> unit
 
-(** [Not_found] is raised is no names are defined for [r] *)
-val arguments_names : global_reference -> Name.t list list
+(** [Not_found] is raised if no names are defined for [r] *)
+val arguments_names : global_reference -> Name.t list
 
 val rename_type_of_constant : env -> pconstant -> types
 val rename_type_of_inductive : env -> pinductive -> types
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 934cefbfe7..d5b125135e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -67,10 +67,11 @@ let error_wrong_numarg_inductive ?loc env c n =
 
 let list_try_compile f l =
   let rec aux errors = function
-  | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors)
+  | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors)
   | h::t ->
       try f h
       with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
+	    let e = CErrors.push e in
 	    aux (e::errors) t in
   aux [] l
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3045d66b80..3ef0bb1b35 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1179,9 +1179,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       (* Some head evar have been instantiated, or unknown kind of problem *)
       evar_conv_x ts env evd pbty t1 t2
 
+let error_cannot_unify env evd pb ?reason t1 t2 =
+  Pretype_errors.error_cannot_unify
+    ~loc:(loc_of_conv_pb evd pb) env
+    evd ?reason (t1, t2)
+
 let check_problems_are_solved env evd =
   match snd (extract_all_conv_pbs evd) with
-  | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2)
+  | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
   | _ -> ()
 
 let max_undefined_with_candidates evd =
@@ -1250,17 +1255,15 @@ let consider_remaining_unif_problems env
 	      aux evd pbs progress (pb :: stuck)
             end
         | UnifFailure (evd,reason) ->
-	    Pretype_errors.error_cannot_unify ~loc:(loc_of_conv_pb evd pb)
-              env evd ~reason (t1, t2))
+           error_cannot_unify env evd pb ~reason t1 t2)
     | _ -> 
 	if progress then aux evd stuck false []
 	else 
 	  match stuck with
 	  | [] -> (* We're finished *) evd
 	  | (pbty,env,t1,t2 as pb) :: _ ->
-	      (* There remains stuck problems *)
-	      Pretype_errors.error_cannot_unify ~loc:(loc_of_conv_pb evd pb)
-                env evd (t1, t2)
+	     (* There remains stuck problems *)
+             error_cannot_unify env evd pb t1 t2
   in
   let (evd,pbs) = extract_all_conv_pbs evd in
   let heuristic_solved_evd = aux evd pbs false [] in