diff options
| author | Arnaud Spiwack | 2014-12-04 13:15:26 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-04 14:38:05 +0100 |
| commit | 964024bf87a87b0e87d8891b3090083ea49b1d03 (patch) | |
| tree | 0d10a2a7e4961be66f3a925b0765b8d42cbdef0f /pretyping | |
| parent | f66b84de608830600e43f6d1a97c29226b6b58ea (diff) | |
Occur-check in refine.
The occur check is done even if the flag [unsafe] is set to true. The rational is that a tactic cannot control where it takes pieces of terms from (and hence will not generally make terms which pass the occur-check), and it would be painful to ask every tactic which takes a term as an argument to do an occur check before [refine].
I reused the same error than used by unification. It gives a pretty nice error message. An alternative would be to have a dedicated error with pretty much the same error message. I'm not sure which is best, so I went for the simplest one.
The same check is done in the compatibility layer.
Fixes a reported bug which I cannot locate for some reason.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 12 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 5 |
2 files changed, 17 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index dd74ecf384..0fcff3d492 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -656,6 +656,18 @@ let check_evars env initial_sigma sigma c = | _ -> iter_constr proc_rec c in proc_rec c +(* spiwack: this is a more complete version of + {!Termops.occur_evar}. The latter does not look recursively into an + [evar_map]. If unification only need to check superficially, tactics + do not have this luxury, and need the more complete version. *) +let occur_evar_upto sigma n c = + let rec occur_rec c = match kind_of_term c with + | Evar (sp,_) when Evar.equal sp n -> raise Occur + | Evar e -> Option.iter occur_rec (existential_opt_value sigma e) + | _ -> iter_constr occur_rec c + in + try occur_rec c; false with Occur -> true + (****************************************) (* Operations on value/type constraints *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index ea00f80673..8e8bbf3679 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -132,6 +132,11 @@ val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t val undefined_evars_of_named_context : evar_map -> named_context -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t +(** [occur_evar_upto sigma k c] returns [true] if [k] appears in + [c]. It looks up recursively in [sigma] for the value of existential + variables. *) +val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool + (** {6 Value/Type constraints} *) val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment |