From b3dbd589e1dc41d7bce18afd87dd6e59968286bb Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 30 Sep 2016 22:50:49 +0200 Subject: Add command 'Set foo Append "bar"' for appending to an option (bug #5109). For now, the only meaningful user is "Set Warnings". Example: Section Bar. Local Set Warnings Append "-foo". (* warning foo is now disabled *) End Bar. (* foo is now reenabled, assuming it was before entering the section *) --- toplevel/vernacentries.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2e2a60c861..e16b9128e4 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1456,6 +1456,9 @@ let vernac_set_option locality key = function | IntValue n -> set_int_option_value_gen locality key n | BoolValue b -> set_bool_option_value_gen locality key b +let vernac_set_append_option locality key s = + set_string_option_append_value_gen locality key s + let vernac_unset_option locality key = unset_option_value_gen locality key @@ -1925,6 +1928,7 @@ let interp ?proof ~loc locality poly c = | VernacSetOpacity qidl -> vernac_set_opacity locality qidl | VernacSetStrategy l -> vernac_set_strategy locality l | VernacSetOption (key,v) -> vernac_set_option locality key v + | VernacSetAppendOption (key,v) -> vernac_set_append_option locality key v | VernacUnsetOption key -> vernac_unset_option locality key | VernacRemoveOption (key,v) -> vernac_remove_option key v | VernacAddOption (key,v) -> vernac_add_option key v @@ -1997,7 +2001,7 @@ let check_vernac_supports_locality c l = | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacSetOption _ | VernacUnsetOption _ + | VernacSetOption _ | VernacSetAppendOption _ | VernacUnsetOption _ | VernacDeclareReduction _ | VernacExtend _ | VernacInductive _) -> () -- cgit v1.2.3 From 14f8db195021e709734ed89d9cb513d1c0db6a93 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 3 Oct 2016 22:12:56 +0200 Subject: Fixing #4970 (confusion between special "{" and non special "{{" in notations). --- toplevel/metasyntax.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 92208e3046..4f41043e87 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1203,7 +1203,10 @@ let contract_notation ntn = let rec aux ntn i = if i <= String.length ntn - 5 then let ntn' = - if String.is_sub "{ _ }" ntn i then + if String.is_sub "{ _ }" ntn i && + (i = 0 || ntn.[i-1] = ' ') && + (i = String.length ntn - 5 || ntn.[i+5] = ' ') + then String.sub ntn 0 i ^ "_" ^ String.sub ntn (i+5) (String.length ntn -i-5) else ntn in -- cgit v1.2.3 From 9e8c57419b473fdb3f9fbb8251d1843ec0e6f884 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 4 Oct 2016 13:27:29 +0200 Subject: Quick fix to #4595 (making notations containing "ltac:" unused for printing). Also getting rid of a global side-effect. --- toplevel/metasyntax.ml | 19 ++++++++----------- toplevel/vernacentries.ml | 3 +-- 2 files changed, 9 insertions(+), 13 deletions(-) (limited to 'toplevel') diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index ce8798c713..42f65dfb52 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -890,12 +890,12 @@ let warn_non_reversible_notation = (fun () -> strbrk "This notation will not be used for printing as it is not reversible.") -let is_not_printable onlyparse noninjective = function +let is_not_printable onlyparse nonreversible = function | NVar _ -> if not onlyparse then warn_notation_bound_to_variable (); true | _ -> - if not onlyparse && noninjective then + if not onlyparse && nonreversible then (warn_non_reversible_notation (); true) else onlyparse @@ -1182,12 +1182,11 @@ let add_notation_in_scope local df c mods scope = let nenv = { ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map recvars; - ninterp_only_parse = false; } in - let (acvars, ac) = interp_notation_constr nenv c in + let (acvars, ac, reversible) = interp_notation_constr nenv c in let interp = make_interpretation_vars recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in + let onlyparse = is_not_printable onlyparse (not reversible) ac in let notation = { notobj_local = local; notobj_scope = scope; @@ -1222,12 +1221,11 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let nenv = { ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map recvars; - ninterp_only_parse = false; } in - let (acvars, ac) = interp_notation_constr ~impls nenv c in + let (acvars, ac, reversible) = interp_notation_constr ~impls nenv c in let interp = make_interpretation_vars recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in + let onlyparse = is_not_printable onlyparse (not reversible) ac in let notation = { notobj_local = local; notobj_scope = scope; @@ -1364,10 +1362,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse = let nenv = { ninterp_var_type = i_vars; ninterp_rec_vars = Id.Map.empty; - ninterp_only_parse = false; } in - let nvars, pat = interp_notation_constr nenv c in - let () = nonprintable := nenv.ninterp_only_parse in + let nvars, pat, reversible = interp_notation_constr nenv c in + let () = nonprintable := not reversible in let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in List.map map vars, pat in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e16b9128e4..d639811c56 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1153,7 +1153,6 @@ let vernac_declare_arguments locality r l nargs flags = let default_env () = { Notation_term.ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; - ninterp_only_parse = false; } let vernac_reserve bl = @@ -1162,7 +1161,7 @@ let vernac_reserve bl = let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in - let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in + let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl -- cgit v1.2.3 From 6cfdf1ca60535f6e9ee6c5e0d5c546d34e803c61 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 5 Oct 2016 17:35:33 +0200 Subject: Fix a bug of Mltop.declare_cache_object. Objects registered through the callback functions were pushed on the libstack before the ML-MODULE object itself, leading to anomalies when the corresponding object was assuming that the ML module was properly defined in any other Coq module requiring the Declare ML command. --- toplevel/mltop.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 0a5b92270f..b6690fe47b 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -411,7 +411,7 @@ let inMLModule : ml_module_object -> obj = let declare_ml_modules local l = let l = List.map mod_of_name l in - Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l}) + Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l}) let print_ml_path () = let l = !coq_mlpath_copy in -- cgit v1.2.3