diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-22 05:32:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:03 +0100 |
| commit | 66eae7fa7f8e1f075a8c84afad48af4d35c4bfaf (patch) | |
| tree | 6b4182ea23965c271dc6483b12a179d3c4404543 /interp/constrintern.ml | |
| parent | 6e1f26a075a48fb32bce32e07d6b58e2f38b97a5 (diff) | |
Notations: Do not consider a non-occurring variable as a binder-only variable.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b52a28029..2761b6528 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2170,8 +2170,9 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in - let vars = Id.Map.map (fun (isonlybinding, sc, typ) -> - (!isonlybinding, out_scope !sc, typ)) vl in + let unused = match reversible with NonInjective ids -> ids | _ -> [] in + let vars = Id.Map.mapi (fun id (isonlybinding, sc, typ) -> + (!isonlybinding && not (List.mem_f Id.equal id unused), out_scope !sc, typ)) vl in (* Returns [a] and the ordered list of variables with their scopes *) vars, a, reversible |