From 66eae7fa7f8e1f075a8c84afad48af4d35c4bfaf Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 22 Nov 2017 05:32:17 +0100 Subject: Notations: Do not consider a non-occurring variable as a binder-only variable. --- interp/constrintern.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'interp/constrintern.ml') 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 -- cgit v1.2.3