Merge branch 'v8.6'

4 files changed, 32 insertions, 17 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index a00e4bab30..aa0ebbb83b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -149,6 +149,12 @@ end) = struct
     | GType [] -> tag_type (str "Type")
     | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
 
+  let pr_glob_level = function
+    | GProp -> tag_type (str "Prop")
+    | GSet -> tag_type (str "Set")
+    | GType None -> tag_type (str "Type")
+    | GType (Some (_, u)) -> tag_type (str u)
+
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
     let id = tag_ref (pr_id id) in
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index a59fc6d67d..3de0d805c4 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -44,6 +44,7 @@ module type Pp = sig
   val pr_qualid : qualid -> std_ppcmds
   val pr_patvar : patvar -> std_ppcmds
 
+  val pr_glob_level : glob_level -> std_ppcmds
   val pr_glob_sort : glob_sort -> std_ppcmds
   val pr_guard_annot : (constr_expr -> std_ppcmds) ->
     local_binder list ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 51fc289b46..1cdf55ac6f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -365,8 +365,8 @@ module Make
     | SetAssoc NonA -> keyword "no associativity"
     | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
     | SetOnlyPrinting -> keyword "only printing"
-    | SetOnlyParsing Flags.Current -> keyword "only parsing"
-    | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
+    | SetOnlyParsing -> keyword "only parsing"
+    | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
     | SetFormat("text",s) -> keyword "format " ++ pr_located qs s
     | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s
 
@@ -836,7 +836,8 @@ module Make
         )
       | VernacConstraint v ->
         let pr_uconstraint (l, d, r) =
-          pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r
+          pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+            pr_glob_level r
         in
         return (
           hov 2 (keyword "Constraint" ++ spc () ++
@@ -1000,13 +1001,13 @@ module Make
         )
       | VernacHints (_, dbnames,h) ->
         return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
-      | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) ->
+      | VernacSyntacticDefinition (id,(ids,c),_,compat) ->
         return (
           hov 2
             (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
                prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
                pr_syntax_modifiers
-               (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
+               (match compat with None -> [] | Some v -> [SetCompatVersion v]))
         )
       | VernacDeclareImplicits (q,[]) ->
         return (
@@ -1027,16 +1028,18 @@ module Make
               pr_smart_global q ++
               let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
               let pr_if b x = if b then x else str "" in
-              let pr_br imp max x = match imp, max with
-                | true, false -> str "[" ++ x ++ str "]"
-                | true, true -> str "{" ++ x ++ str "}"
-                | _ -> x in
+              let pr_br imp x = match imp with
+                | `Implicit -> str "[" ++ x ++ str "]"
+                | `MaximallyImplicit -> str "{" ++ x ++ str "}"
+                | `NotImplicit -> x in
               let rec aux n l =
                 match n, l with
                   | 0, l -> spc () ++ str"/" ++ aux ~-1 l
                   | _, [] -> mt()
-                  | n, (id,k,s,imp,max) :: tl ->
-                    spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+                  | n, { name = id; recarg_like = k;
+                         notation_scope = s;
+                         implicit_status = imp } :: tl ->
+                    spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
                       aux (n-1) tl in
               prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
                 (if not (List.is_empty mods) then str" : " else str"") ++
diff --git a/printing/printmod.ml b/printing/printmod.ml
index c939f54e80..dfa66d4376 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -247,19 +247,24 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with
   | _ -> raise Not_found
 
 let nametab_register_modparam mbid mtb =
+  let id = MBId.to_id mbid in
   match mtb.mod_type with
-  | MoreFunctor _ -> () (* functorial param : nothing to register *)
+  | MoreFunctor _ -> id (* functorial param : nothing to register *)
   | NoFunctor struc ->
     (* We first try to use the algebraic type expression if any,
        via a Declaremods function that converts back to module entries *)
     try
-      Declaremods.process_module_binding mbid (get_typ_expr_alg mtb)
+      let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in
+      id
     with e when CErrors.noncritical e ->
       (* Otherwise, we try to play with the nametab ourselves *)
       let mp = MPbound mbid in
-      let dir = DirPath.make [MBId.to_id mbid] in
+      let check id = Nametab.exists_dir (DirPath.make [id]) in
+      let id = Namegen.next_ident_away_from id check in
+      let dir = DirPath.make [id] in
       nametab_register_dir mp;
-      List.iter (nametab_register_body mp dir) struc
+      List.iter (nametab_register_body mp dir) struc;
+      id
 
 let print_body is_impl env mp (l,body) =
   let name = pr_label l in
@@ -353,7 +358,7 @@ let print_mod_expr env mp locals = function
 let rec print_functor fty fatom is_type env mp locals = function
   |NoFunctor me -> fatom is_type env mp locals me
   |MoreFunctor (mbid,mtb1,me2) ->
-      nametab_register_modparam mbid mtb1;
+      let id = nametab_register_modparam mbid mtb1 in
       let mp1 = MPbound mbid in
       let pr_mtb1 = fty env mp1 locals mtb1 in
       let env' = Option.map (Modops.add_module_type mp1 mtb1) env in
@@ -361,7 +366,7 @@ let rec print_functor fty fatom is_type env mp locals = function
       let kwd = if is_type then "Funsig" else "Functor" in
       hov 2
         (keyword kwd ++ spc () ++
-	 str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++
+	 str "(" ++ pr_id id ++ str ":" ++ pr_mtb1 ++ str ")" ++
 	 spc() ++ print_functor fty fatom is_type env' mp locals' me2)
 
 let rec print_expression x =