From 9cbe6fedf81f85430290ca690d8995f3694b59c3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 24 Dec 2014 17:50:13 +0100
Subject: Simplifying second_order_matching: no need to invert the linear
 initial segment of the context of the evar.

---
 pretyping/evarconv.ml    | 4 ++--
 pretyping/unification.ml | 3 ++-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0b6ead8c6f..c20235f539 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -985,8 +985,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       let filter' = filter_possible_projections c ty ctxt args in
       let filter = Filter.map_along (&&) filter filter' in
       (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt',l,occsl)
-  | [], [], [] -> []
-  | _ -> anomaly (Pp.str "Signature, instance and occurrences list do not match") in
+  | _, _, [] -> []
+  | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in
 
   let rec set_holes evdref rhs = function
   | (id,_,c,cty,evsref,filter,occs)::subst ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5f3ea7a98d..67e9001bb5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -107,7 +107,8 @@ let set_occurrences_of_last_arg args =
 let abstract_list_all_with_dependencies env evd typ c l =
   let evd,ev = new_evar env evd typ in
   let evd,ev' = evar_absorb_arguments env evd (destEvar ev) l in
-  let argoccs = set_occurrences_of_last_arg (snd ev') in
+  let n = List.length l in
+  let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
   let evd,b =
     Evarconv.second_order_matching empty_transparent_state
       env evd ev' argoccs c in
-- 
cgit v1.2.3