diff options
| author | Matthieu Sozeau | 2017-07-28 01:35:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:12:27 +0100 |
| commit | dc8f191f2d81fd5f851b84e7aeda487df584197e (patch) | |
| tree | 3eb0154ad669b8737dec57c3d04421821893dd8a | |
| parent | 1c9e1a39652b401805029519055aa62adacde339 (diff) | |
unification: abstract_list_all_with_dependencies fix
For second_order_matching call, prefer abstraction of evar arguments,
and use same test as original (just eq_constr)
| -rw-r--r-- | pretyping/unification.ml | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6bb999c3f5..8d8313eeff 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -142,7 +142,14 @@ let abstract_list_all env evd typ c l = let set_occurrences_of_last_arg args = Evarconv.AtOccurrences AllOccurrences :: - List.tl (Array.map_to_list (fun _ -> Evarconv.default_occurrence_selection) args) + List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified true) args) + +let occurrence_test _ _ _ env sigma _ c1 c2 = + match EConstr.eq_constr_universes env sigma c1 c2 with + | None -> false, sigma + | Some cstr -> + try true, Evd.add_universe_constraints sigma cstr + with UniversesDiffer -> false, sigma let abstract_list_all_with_dependencies env evd typ c l = let (evd, ev) = new_evar env evd typ in @@ -150,8 +157,9 @@ let abstract_list_all_with_dependencies env evd typ c l = 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 (Evarconv.default_flags_of TransparentState.empty) - env evd ev' (Evarconv.default_occurrence_test ~frozen_evars:Evar.Set.empty TransparentState.empty, argoccs) c in + Evarconv.second_order_matching + (Evarconv.default_flags_of TransparentState.empty) + env evd ev' (occurrence_test, argoccs) c in if b then let p = nf_evar evd ev in evd, p |