aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-24 13:46:43 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 21:55:44 +0200
commit361cc73acc9d016e183e3fe85a84f470c31bc4e2 (patch)
tree5a321fe44123a1914f433a12a9027257079d10f9 /intf
parentc96824b7d1043090747926e2e3fa369f5d3822ff (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.mli2
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 }