diff options
| -rw-r--r-- | engine/evd.ml | 8 | ||||
| -rw-r--r-- | engine/evd.mli | 6 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 21 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 3 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
5 files changed, 25 insertions, 15 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 2d28892e6e..a89a67c287 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -128,11 +128,15 @@ end module Abstraction = struct - type t = bool list + type abstraction = + | Abstract + | Imitate + + type t = abstraction list let identity = [] - let abstract_last l = true :: l + let abstract_last l = Abstract :: l end (* The kinds of existential variables are now defined in [Evar_kinds] *) diff --git a/engine/evd.mli b/engine/evd.mli index 1f6a0da882..fcccb1be5a 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -78,7 +78,11 @@ sig end module Abstraction : sig - type t = bool list + type abstraction = + | Abstract + | Imitate + + type t = abstraction list val identity : t diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 99c32e06ee..95301fb9ca 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1127,16 +1127,14 @@ type occurrence_match_test = env -> evar_map -> constr -> env -> evar_map -> int -> constr -> constr -> bool * evar_map -type prefer_abstraction = bool - type occurrence_selection = | AtOccurrences of Locus.occurrences - | Unspecified of prefer_abstraction + | Unspecified of Abstraction.abstraction type occurrences_selection = occurrence_match_test * occurrence_selection list -let default_occurrence_selection = Unspecified false +let default_occurrence_selection = Unspecified Abstraction.Imitate let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat = let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in @@ -1406,7 +1404,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = raise (TypingFailed evd); let evd = Evd.define ev (EConstr.of_constr t) evd in check_evar_instance evd ev (EConstr.of_constr t) (conv_fun evar_conv_x flags) - | Some l when abstract && List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> + | Some l when abstract = Abstraction.Abstract && + List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> let evd = Evd.define ev vid evd in check_evar_instance evd ev vid (conv_fun evar_conv_x flags) | _ -> evd) @@ -1468,10 +1467,14 @@ let default_evar_selection flags evd (ev,args) = let rec aux args abs = match args, abs with | _ :: args, a :: abs -> - let spec = if not flags.allow_K_at_toplevel then - AtOccurrences (if a then Locus.AtLeastOneOccurrence else Locus.AllOccurrences) - else Unspecified a in - spec :: aux args abs + let spec = + if not flags.allow_K_at_toplevel then + let occs = + if a == Abstraction.Abstract then Locus.AtLeastOneOccurrence + else Locus.AllOccurrences + in AtOccurrences occs + else Unspecified a + in spec :: aux args abs | l, [] -> List.map (fun _ -> default_occurrence_selection) l | [], _ :: _ -> assert false in aux (Array.to_list args) evi.evar_abstract_arguments diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 994576c45b..c2ad4e6678 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -80,11 +80,10 @@ type occurrence_match_test = (** When given the choice of abstracting an occurrence or leaving it, force abstration. *) -type prefer_abstraction = bool type occurrence_selection = | AtOccurrences of occurrences - | Unspecified of prefer_abstraction + | Unspecified of Abstraction.abstraction (** By default, unspecified, not preferring abstraction. This provides the most general solutions. *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8d8313eeff..486aa38558 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -142,7 +142,7 @@ 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.Unspecified true) args) + List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified Abstraction.Abstract) args) let occurrence_test _ _ _ env sigma _ c1 c2 = match EConstr.eq_constr_universes env sigma c1 c2 with |