diff options
| author | Hugo Herbelin | 2016-04-24 13:46:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:44 +0200 |
| commit | 361cc73acc9d016e183e3fe85a84f470c31bc4e2 (patch) | |
| tree | 5a321fe44123a1914f433a12a9027257079d10f9 /ltac/tacinterp.ml | |
| 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 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 02b03b72c2..9b41a276b9 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -678,7 +678,7 @@ let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist = let interp_pure_open_constr ist = interp_gen WithoutTypeConstraint ist false pure_open_constr_flags -let interp_typed_pattern ist env sigma (c,_) = +let interp_typed_pattern ist env sigma (_,c,_) = let sigma, c = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in pattern_of_constr env sigma c @@ -1106,12 +1106,11 @@ let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt (* Reads a pattern by substituting vars of lfun *) let use_types = false -let eval_pattern lfun ist env sigma ((glob,_),pat as c) = - let bound_names = bound_glob_vars glob in +let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) = if use_types then - (bound_names,interp_typed_pattern ist env sigma c) + (bvars,interp_typed_pattern ist env sigma c) else - (bound_names,instantiate_pattern env sigma lfun pat) + (bvars,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) |