Merge branch 'v8.5'

4 files changed, 7 insertions, 7 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 19c85c9e27..121ab74885 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -415,8 +415,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
           try_aux sub mk_ctx next
   | Case (ci,hd,c1,lc) ->
       let next_mk_ctx = function
-      | [] -> assert false
-      | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | _ -> assert false
       in
       let sub = (env, c1) :: (env, hd) :: subargs env lc in
       try_aux sub next_mk_ctx next
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 754ad8f588..bbc4f1db29 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1484,7 +1484,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
     if occur_meta body then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar evk body then raise (OccurCheckIn (evd',body));
+    if occur_evar_upto evd' evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
     let evd', body = refresh_universes pbty env evd' body in
 (* Cannot strictly type instantiations since the unification algorithm
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 5ae989b789..1c3ae9ad95 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -520,7 +520,7 @@ let rec check_and_clear_in_constr env evdref err ids c =
 let clear_hyps_in_evi_main env evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
-     the contexts of the evars occuring in evi *)
+     the contexts of the evars occurring in evi *)
   let terms =
     List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
   let nhyps =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8a5db90590..48911a5a9f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1011,8 +1011,8 @@ let contextually byhead occs f env sigma t =
     snd (e_contextually byhead occs f' env sigma t)
 
 (* linear bindings (following pretty-printer) of the value of name in c.
- * n is the number of the next occurence of name.
- * ol is the occurence list to find. *)
+ * n is the number of the next occurrence of name.
+ * ol is the occurrence list to find. *)
 
 let match_constr_evaluable_ref sigma c evref = 
   match kind_of_term c, evref with
@@ -1061,7 +1061,7 @@ let is_projection env = function
 
 (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
- * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
+ * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env sigma (occs,name) c =
   let unfo nowhere_except_in locs =