Merge branch 'v8.6'

3 files changed, 19 insertions, 16 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ec45c7ed8..f28ef3f65 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -899,12 +899,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
 
@@ -1102,7 +1102,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
@@ -1191,12 +1194,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;
@@ -1231,12 +1233,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;
@@ -1373,10 +1374,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/mltop.ml b/toplevel/mltop.ml
index 6b62f7aeb..2396cf04a 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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3b14f597c..9415ade28 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1154,7 +1154,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 =
@@ -1163,7 +1162,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
 
@@ -1457,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
 
@@ -1926,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
@@ -1998,7 +2001,7 @@ let check_vernac_supports_locality c l =
     | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacSetOption _ | VernacUnsetOption _
+    | VernacSetOption _ | VernacSetAppendOption _ | VernacUnsetOption _
     | VernacDeclareReduction _
     | VernacExtend _ 
     | VernacInductive _) -> ()