diff options
| author | Hugo Herbelin | 2017-08-14 01:18:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-12 20:30:11 +0200 |
| commit | bc3b07f639f04295bc440f42d5aa2420c07ecee6 (patch) | |
| tree | 482bdba33eacab517e116520448a145311a2e410 /interp/notation_ops.ml | |
| parent | 5d3d60e88f137183b4155bfa446dc7f3ebb35993 (diff) | |
Fixing a typo in printing notations with recursive binders.
Was causing a failure to print recursive binders used twice or more in
the same notation.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 99e18f09ef..f605729217 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -824,7 +824,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) alp, b :: bl | _ -> raise No_match in let alp, bl = unify alp bl bl' in - let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in alp, add_bindinglist_env sigma var bl with Not_found -> alp, add_bindinglist_env sigma var bl |