diff options
| -rw-r--r-- | interp/constrintern.ml | 12 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations3.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 12 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
7 files changed, 29 insertions, 10 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 158ac24b2..694bec897 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -273,8 +273,8 @@ let error_expect_binder_notation_type ?loc id = let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = try - let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in - if istermvar then isonlybinding := false; + let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in + if not istermvar then used_as_binder := true; let () = if istermvar then (* scopes have no effect on the interpretation of identifiers *) begin match !idscopes with @@ -1997,7 +1997,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | Some gen -> let (ltacvars, ntnvars) = lvar in (* Preventively declare notation variables in ltac as non-bindings *) - Id.Map.iter (fun x (isonlybinding,_,_) -> isonlybinding := false) ntnvars; + Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars; let ntnvars = Id.Map.domain ntnvars in let extra = ltacvars.ltac_extra in let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in @@ -2302,7 +2302,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in + let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize (Global.env()) {ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impls} @@ -2313,8 +2313,8 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l 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)) vl in + let vars = Id.Map.mapi (fun id (used_as_binder, sc, typ) -> + (!used_as_binder && not (List.mem_f Id.equal id unused), out_scope !sc)) vl in (* Returns [a] and the ordered list of variables with their scopes *) vars, a, reversible diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 0b5009e26..d16c9bb80 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -214,7 +214,7 @@ type proof_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level - | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index cca1b2989..d90fd3eb7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1174,7 +1174,8 @@ GEXTEND Gram | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) - | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,lev) + | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev) + | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None) | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) ] ] ; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2fc7843ed..31c0d20f3 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -383,7 +383,7 @@ open Decl_kinds prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n | SetItemLevelAsBinder (l,bk,n) -> prlist_with_sep sep_v2 str l ++ - spc() ++ pr_at_level n ++ spc() ++ pr_constr_as_binder_kind bk + spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk | SetLevel n -> pr_at_level (NumLevel n) | SetAssoc LeftA -> keyword "left associativity" | SetAssoc RightA -> keyword "right associativity" diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 3fd4c1c31..436e97e9f 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -219,3 +219,9 @@ fun p : nat => if p is S n then n else 0 : nat -> nat fun p : comparison => if p is Lt then 1 else 0 : comparison -> nat +fun S : nat => [S | S + S] + : nat -> nat * (nat -> nat) +fun N : nat => [N | N + 0] + : nat -> nat * (nat -> nat) +fun S : nat => [[S | S + S]] + : nat -> nat * (nat -> nat) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 9ea218481..df3d86793 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -389,3 +389,15 @@ Notation "'if' c 'is' p 'then' u 'else' v" := (at level 200, p pattern at level 100). Check fun p => if p is S n then n else 0. Check fun p => if p is Lt then 1 else 0. + +(* Check that mixed binders and terms defaults to ident and not pattern *) +Module E. + (* First without an indirection *) +Notation "[ n | t ]" := (n, (fun n : nat => t)). +Check fun S : nat => [ S | S+S ]. +Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *) + (* Then with an indirection *) +Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)). +Notation "[[ n | t ]]" := [[ n | n | t ]]. +Check fun S : nat => [[ S | S+S ]]. +End E. diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 524c9b32b..bcffe640c 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -831,7 +831,7 @@ let interp_modifiers modl = let open NotationMods in if Id.List.mem_assoc id acc.etyps then user_err ~hdr:"Metasyntax.interp_modifiers" (str s ++ str " is already assigned to an entry or constr level."); - let typ = ETConstrAsBinder (bk,Some n) in + let typ = ETConstrAsBinder (bk,n) in interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l) | SetLevel n :: l -> interp { acc with level = Some n; } l |