diff options
| author | Maxime Dénès | 2017-03-28 18:15:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-28 18:16:41 +0200 |
| commit | dc8d8daf8850ff1a414ae36c860bc925d87eab01 (patch) | |
| tree | 99fafdf4d04dcd9fe6eb15d3b561624a5344702d | |
| parent | 98e51078fa624ce780b16d8e372ef33ac97ffaee (diff) | |
Revert to incorrect heuristic in apply.
Was breaking e.g. fiat-crypto.
| -rw-r--r-- | pretyping/unification.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8824c06abd..611d165fe1 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -64,6 +64,18 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } +(** Making this unification algorithm correct w.r.t. the evar-map abstraction + breaks too much stuff. So we redefine incorrect functions here. *) + +let unsafe_occur_meta_or_existential c = + let c = EConstr.Unsafe.to_constr c in + let rec occrec c = match kind_of_term c with + | Evar _ -> raise Occur + | Meta _ -> raise Occur + | _ -> iter_constr occrec c + in try occrec c; false with Occur -> true + + let occur_meta_or_undefined_evar evd c = (** This is performance-critical. Using the evar-insensitive API changes the resulting heuristic. *) @@ -1880,7 +1892,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = else let allow_K = flags.allow_K_in_toplevel_higher_order_unification in let flags = - if occur_meta_or_existential evd op || !keyed_unification then + if unsafe_occur_meta_or_existential op || !keyed_unification then (* This is up to delta for subterms w/o metas ... *) flags else |