diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-24 17:50:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-30 15:57:45 +0100 |
| commit | 9cbe6fedf81f85430290ca690d8995f3694b59c3 (patch) | |
| tree | 9c7cfa0b202b72a920551e9ffdbf2c41f34b0261 | |
| parent | ee0aeee014f1111781c0e616c3f72243a03df1ea (diff) | |
Simplifying second_order_matching: no need to invert the linear
initial segment of the context of the evar.
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 3 |
2 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0b6ead8c6..c20235f53 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 5f3ea7a98..67e9001bb 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 |