diff options
| author | Hugo Herbelin | 2016-07-19 10:44:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-19 11:45:48 +0200 |
| commit | b663b735adaf546192ff5b25b608dda55e05f3d8 (patch) | |
| tree | 1e9c391964bd85dcd03b4ac209a91989b6a4a5ad /interp/notation_ops.ml | |
| parent | b3e7ef09210267e6d34bc1ac377e66c7fec7e739 (diff) | |
Notations with multiple recursive binders: fixing use of alpha-conversion.
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 8045213459..1b84ccff48 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -779,8 +779,8 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) match bl, bl' with | [], [] -> alp, [] | b :: bl, b' :: bl' -> - let alp,bl = unify alp bl bl' in let alp,b = unify_binder alp b b' in + let alp,bl = unify alp bl bl' in alp, b :: bl | _ -> raise No_match in let alp, bl = unify alp bl bl' in |