diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-24 13:46:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:44 +0200 |
| commit | 361cc73acc9d016e183e3fe85a84f470c31bc4e2 (patch) | |
| tree | 5a321fe44123a1914f433a12a9027257079d10f9 /intf | |
| parent | c96824b7d1043090747926e2e3fa369f5d3822ff (diff) | |
Attempt to slightly improve abusive "Collision between bound
variables" when matching over "{v : _ | _ & _}" which hides twice the
binding "fun v" since it is "sig2 (fun v => _) (fun v => _)".
Computing the bound variables statically at internalisation time
rather than every time at interpretation time. This cannot hurt even
if I don't know how to deal with the "notation" problem of a single
bound variable actually hiding two: at the current time, the notation
is printed only if the two variables are identical (see #4592), so,
with this semantics the warning should not be printed, but we lost the
information that we are coming from a notation; if #4592 were
addressed, then one of the binding should be alpha-renamed if they
differ, so collision should be solved by choosing the variable name
which is not renamed, but the matching algorithm should then be aware
of what the notation printing algorithm is doing... maybe not the most
critical thing at the current time.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 875ad3d16..e06436d8a 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -120,7 +120,7 @@ type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Id.Set.t -type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern +type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern type 'a delayed_open = 'a Pretyping.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } |