16 files changed, 829 insertions, 216 deletions

diff --git a/Makefile.make b/Makefile.make
index e19053462d..e63a578e37 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -56,6 +56,7 @@ FIND_SKIP_DIRS:=-not -name . '(' \
   -name "$${GIT_DIR}" -o \
   -name '_build' -o \
   -name '_build_ci' -o \
+  -name '_build_boot' -o \
   -name '_install_ci' -o \
   -name 'gramlib' -o \
   -name 'user-contrib' -o \
@@ -251,7 +252,7 @@ docclean:
 	rm -rf doc/sphinx/_build
 
 archclean: clean-ide optclean voclean plugin-tutorialclean
-	rm -rf _build
+	rm -rf _build _build_boot
 	rm -f $(ALLSTDLIB).*
 
 optclean:
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index 2af4b58201..9ce5da9f50 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -6,8 +6,8 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download fiat_crypto_legacy
 
-fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display"
-fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded"
+fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
   ./etc/ci/remove_autogenerated.sh && \
diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py
index 91f0a7cb1b..feafcba026 100644
--- a/doc/tools/coqrst/checkdeps.py
+++ b/doc/tools/coqrst/checkdeps.py
@@ -10,13 +10,20 @@
 from __future__ import print_function
 import sys
 
+missing_deps = []
+
 def eprint(*args, **kwargs):
     print(*args, file=sys.stderr, **kwargs)
 
 def missing_dep(dep):
-    eprint('Cannot find %s (needed to build documentation)' % dep)
-    eprint('You can run `pip3 install %s` to install it.' % dep)
-    sys.exit(1)
+    missing_deps.append(dep)
+
+def report_missing_deps():
+    if len(missing_deps) > 0:
+        deps = " ".join(missing_deps)
+        eprint('Cannot find package(s) `%s` (needed to build documentation)' % deps)
+        eprint('You can run `pip3 install %s` to install it/them.' % deps)
+        sys.exit(1)
 
 try:
     import sphinx_rtd_theme
@@ -37,3 +44,10 @@ try:
     import bs4
 except:
     missing_dep('beautifulsoup4')
+
+try:
+    import sphinxcontrib.bibtex
+except:
+    missing_dep('sphinxcontrib-bibtex')
+
+report_missing_deps()
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 16be96454e..b0ea75ac60 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -302,7 +302,8 @@ let tclONCE = Proof.once
 
 exception MoreThanOneSuccess
 let _ = CErrors.register_handler begin function
-  | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.")
+  | MoreThanOneSuccess ->
+    Pp.str "This tactic has more than one success."
   | _ -> raise CErrors.Unhandled
 end
 
@@ -347,8 +348,7 @@ exception NoSuchGoals of int
 
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
-    CErrors.user_err
-      (str "No such " ++ str (String.plural n "goal") ++ str ".")
+    str "No such " ++ str (String.plural n "goal") ++ str "."
   | _ -> raise CErrors.Unhandled
 end
 
@@ -420,12 +420,9 @@ let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
 exception SizeMismatch of int*int
 let _ = CErrors.register_handler begin function
   | SizeMismatch (i,j) ->
-      let open Pp in
-      let errmsg =
-        str"Incorrect number of goals" ++ spc() ++
-        str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
-      in
-      CErrors.user_err  errmsg
+    let open Pp in
+    str"Incorrect number of goals" ++ spc() ++
+    str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
   | _ -> raise CErrors.Unhandled
 end
 
@@ -910,7 +907,8 @@ let tclPROGRESS t =
     tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
 
 let _ = CErrors.register_handler begin function
-  | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Logic_monad.Tac_Timeout ->
+    Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!"
   | _ -> raise CErrors.Unhandled
 end
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cc0c1e4602..c55e17e7a3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -281,6 +281,17 @@ let get_extern_reference () = !my_extern_reference
 let extern_reference ?loc vars l = !my_extern_reference vars l
 
 (**********************************************************************)
+(* utilities                                                          *)
+
+let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) =
+  match args, subscopes with
+  | [], _ -> []
+  | a :: args, scopt :: subscopes ->
+    (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all
+  | a :: args, [] ->
+    (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all
+
+(**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
 
 let add_patt_for_params ind l =
@@ -550,14 +561,14 @@ let is_gvar id c = match DAst.get c with
 | GVar id' -> Id.equal id id'
 | _ -> false
 
-let is_projection nargs = function
-  | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
-    (try
-       let n = Recordops.find_projection_nparams r + 1 in
-         if n <= nargs then Some n
-         else None
-     with Not_found -> None)
-  | _ -> None
+let is_projection nargs r =
+  if not !Flags.in_debugger && not !Flags.raw_print && !print_projections then
+    try
+      let n = Recordops.find_projection_nparams r + 1 in
+      if n <= nargs then Some n
+      else None
+    with Not_found -> None
+  else None
 
 let is_hole = function CHole _ | CEvar _ -> true | _ -> false
 
@@ -569,11 +580,12 @@ let is_needed_for_correct_partial_application tail imp =
 
 exception Expl
 
-(* Implicit args indexes are in ascending order *)
-(* inctx is useful only if there is a last argument to be deduced from ctxt *)
-let explicitize inctx impl (cf,f) args =
-  let impl = if !Constrintern.parsing_explicit then [] else impl in
-  let n = List.length args in
+(* Take a list of arguments starting at position [q] and their implicit status *)
+(* Decide for each implicit argument if it skipped or made explicit *)
+(* If the removal of implicit arguments is not possible, raise [Expl] *)
+(* [inctx] tells if the term is in a context which will enforce the external type *)
+(* [n] is the total number of arguments block to which the [args] belong *)
+let adjust_implicit_arguments inctx n q args impl =
   let rec exprec q = function
     | a::args, imp::impl when is_status_implicit imp ->
         let tail = exprec (q+1) (args,impl) in
@@ -595,10 +607,11 @@ let explicitize inctx impl (cf,f) args =
       (* The non-explicit application cannot be parsed back with the same type *)
       raise Expl
     | [], _ -> []
-  in
+  in exprec q (args,impl)
+
+let extern_projection (cf,f) args impl =
   let ip = is_projection (List.length args) cf in
-  let expl () =
-    match ip with
+  match ip with
     | Some i ->
       (* Careful: It is possible to have declared implicits ending
          before the principal argument *)
@@ -607,33 +620,61 @@ let explicitize inctx impl (cf,f) args =
         with Failure _ -> false
       in
       if is_impl
-      then raise Expl
+      then None
       else
         let (args1,args2) = List.chop i args in
         let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in
-        let args1 = exprec 1 (args1,impl1) in
-        let args2 = exprec (i+1) (args2,impl2) in
-        let ip = Some (List.length args1) in
-          CApp ((ip,f),args1@args2)
-    | None ->
-      let args = exprec 1 (args,impl) in
-        if List.is_empty args then f.CAst.v else
-          match f.CAst.v with
-          | CApp (g,args') ->
-              (* may happen with notations for a prefix of an n-ary
-                 application *)
-              CApp (g,args'@args)
-          | _ -> CApp ((None, f), args) in
-    try expl ()
-    with Expl ->
-      let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in
-      let ip = if !print_projections then ip else None in
-        CAppExpl ((ip, f', us), List.map Lazy.force args)
+        Some (i,(args1,impl1),(args2,impl2))
+    | None -> None
 
 let is_start_implicit = function
   | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
   | [] -> false
 
+let extern_record ref args =
+  try
+    if !Flags.raw_print then raise Exit;
+    let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
+    let struc = Recordops.lookup_structure (fst cstrsp) in
+    if PrintingRecord.active (fst cstrsp) then
+      ()
+    else if PrintingConstructor.active (fst cstrsp) then
+      raise Exit
+    else if not (get_record_print ()) then
+      raise Exit;
+    let projs = struc.Recordops.s_PROJ in
+    let locals = struc.Recordops.s_PROJKIND in
+    let rec cut args n =
+      if Int.equal n 0 then args
+      else
+        match args with
+        | [] -> raise No_match
+        | _ :: t -> cut t (n - 1) in
+    let args = cut args struc.Recordops.s_EXPECTEDPARAM in
+    let rec ip projs locs args acc =
+      match projs with
+      | [] -> acc
+      | None :: q -> raise No_match
+      | Some c :: q ->
+         match locs with
+         | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
+         | { Recordops.pk_true_proj = false } :: locs' ->
+            (* we don't want to print locals *)
+            ip q locs' args acc
+         | { Recordops.pk_true_proj = true } :: locs' ->
+            match args with
+            | [] -> raise No_match
+            (* we give up since the constructor is not complete *)
+            | arg :: tail ->
+               let arg = Lazy.force arg in
+               let loc = arg.CAst.loc in
+               let ref = extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c) in
+               ip q locs' tail ((ref, arg) :: acc)
+    in
+    Some (List.rev (ip projs locals args []))
+  with
+    | Not_found | No_match | Exit -> None
+
 let extern_global impl f us =
   if not !Constrintern.parsing_explicit && is_start_implicit impl
   then
@@ -641,26 +682,63 @@ let extern_global impl f us =
   else
     CRef (f,us)
 
-let extern_app inctx impl (cf,f) us args =
-  if List.is_empty args then
-    (* If coming from a notation "Notation a := @b" *)
-    CAppExpl ((None, f, us), [])
-  else if not !Constrintern.parsing_explicit &&
-    ((!Flags.raw_print ||
-      (!print_implicits && not !print_implicits_explicit_args)) &&
-     List.exists is_status_implicit impl)
-  then
+(* Implicit args indexes are in ascending order *)
+(* inctx is useful only if there is a last argument to be deduced from ctxt *)
+let extern_applied_ref inctx impl (cf,f) us args =
+  let isproj = is_projection (List.length args) cf in
+  try
+    if not !Constrintern.parsing_explicit &&
+       ((!Flags.raw_print ||
+         (!print_implicits && not !print_implicits_explicit_args)) &&
+        List.exists is_status_implicit impl)
+    then raise Expl;
+    let impl = if !Constrintern.parsing_explicit then [] else impl in
+    let n = List.length args in
+    let ref = CRef (f,us) in
+    let f = CAst.make ref in
+    match extern_projection (cf,f) args impl with
+    (* Try a [t.(f args1) args2] projection-style notation *)
+    | Some (i,(args1,impl1),(args2,impl2)) ->
+      let args1 = adjust_implicit_arguments inctx n 1 args1 impl1 in
+      let args2 = adjust_implicit_arguments inctx n (i+1) args2 impl2 in
+      let ip = Some (List.length args1) in
+      CApp ((ip,f),args1@args2)
+      (* A normal application node with each individual implicit
+         arguments either dropped or made explicit *)
+    | None ->
+      let args = adjust_implicit_arguments inctx n 1 args impl in
+      if args = [] then ref else CApp ((None, f), args)
+  with Expl ->
+  (* A [@f args] node *)
     let args = List.map Lazy.force args in
-    CAppExpl ((is_projection (List.length args) cf,f,us), args)
-  else
-    explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args
+    let isproj = if !print_projections then isproj else None in
+    CAppExpl ((isproj,f,us), args)
 
-let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = match args, subscopes with
-| [], _ -> []
-| a :: args, scopt :: subscopes ->
-  (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all
-| a :: args, [] ->
-  (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all
+let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs =
+  try
+    let syndefargs = List.map (fun a -> (a,None)) syndefargs in
+    let extraargs = adjust_implicit_arguments false (List.length extraargs) 1 extraargs extraimpl in
+    let args = syndefargs @ extraargs in
+    if args = [] then cf else CApp ((None, CAst.make cf), args)
+  with Expl ->
+    let args = syndefargs @ List.map Lazy.force extraargs in
+    CAppExpl ((None,f,None), args)
+
+let mkFlattenedCApp (head,args) =
+  match head.CAst.v with
+  | CApp (g,args') ->
+    (* may happen with notations for a prefix of an n-ary application *)
+    (* or after removal of a coercion to funclass *)
+    CApp (g,args'@args)
+  | _ ->
+    CApp ((None, head), args)
+
+let extern_applied_notation n impl f args =
+  if List.is_empty args then
+    f.CAst.v
+  else
+    let args = adjust_implicit_arguments false (List.length args) 1 args impl in
+    mkFlattenedCApp (f,args)
 
 let extern_args extern env args =
   let map (arg, argscopes) = lazy (extern argscopes env arg) in
@@ -838,56 +916,19 @@ let rec extern inctx scopes vars r =
          | GRef (ref,us) ->
              let subscopes = find_arguments_scope ref in
              let args = fill_arg_scopes args subscopes scopes in
-             begin
-               try
-                 if !Flags.raw_print then raise Exit;
-                 let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
-                 let struc = Recordops.lookup_structure (fst cstrsp) in
-                 if PrintingRecord.active (fst cstrsp) then
-                   ()
-                 else if PrintingConstructor.active (fst cstrsp) then
-                   raise Exit
-                 else if not (get_record_print ()) then
-                   raise Exit;
-                 let projs = struc.Recordops.s_PROJ in
-                 let locals = struc.Recordops.s_PROJKIND in
-                 let rec cut args n =
-                   if Int.equal n 0 then args
-                   else
-                     match args with
-                     | [] -> raise No_match
-                     | _ :: t -> cut t (n - 1) in
-                 let args = cut args struc.Recordops.s_EXPECTEDPARAM in
-                 let rec ip projs locs args acc =
-                   match projs with
-                     | [] -> acc
-                     | None :: q -> raise No_match
-                     | Some c :: q ->
-                         match locs with
-                           | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
-                           | { Recordops.pk_true_proj = false } :: locs' ->
-                               (* we don't want to print locals *)
-                               ip q locs' args acc
-                           | { Recordops.pk_true_proj = true } :: locs' ->
-                               match args with
-                                 | [] -> raise No_match
-                                     (* we give up since the constructor is not complete *)
-                                 | (arg, scopes) :: tail ->
-                                     let head = extern true scopes vars arg in
-                                     ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc)
-                   in
-                 CRecord (List.rev (ip projs locals args []))
-               with
-                 | Not_found | No_match | Exit ->
-                    let args = extern_args (extern true) vars args in
-                     extern_app inctx
-                       (select_stronger_impargs (implicits_of_global ref))
-                       (Some ref,extern_reference ?loc vars ref) (extern_universes us) args
-             end
-
-         | _       ->
-           explicitize inctx [] (None,sub_extern false scopes vars f)
-             (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
+             let args = extern_args (extern true) vars args in
+             (* Try a "{|...|}" record notation *)
+             (match extern_record ref args with
+             | Some l -> CRecord l
+             | None ->
+             (* Otherwise... *)
+               extern_applied_ref inctx
+                 (select_stronger_impargs (implicits_of_global ref))
+                 (ref,extern_reference ?loc vars ref) (extern_universes us) args)
+         | _ ->
+             let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in
+             let head = sub_extern false scopes vars f in
+             mkFlattenedCApp (head,args))
 
   | GLetIn (na,b,t,c) ->
       CLetIn (make ?loc na,sub_extern false scopes vars b,
@@ -1104,46 +1145,45 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
       let loc = Glob_ops.loc_of_glob_constr t in
       try
         if is_inactive_rule keyrule then raise No_match;
-        (* Adjusts to the number of arguments expected by the notation *)
-        let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with
-          | GApp (f,args), Some n
-              when List.length args >= n ->
+        let f,args =
+          match DAst.get t with
+          | GApp (f,args) -> f,args
+          | _ -> t,[] in
+        let nallargs = List.length args in
+        let argsscopes,argsimpls =
+          match DAst.get f with
+          | GRef (ref,_) ->
+            let subscopes = find_arguments_scope ref in
+            let impls = select_impargs_size nallargs (implicits_of_global ref) in
+            subscopes, impls
+          | _ ->
+            [], [] in
+        (* Adjust to the number of arguments expected by the notation *)
+        let (t,args,argsscopes,argsimpls) = match n with
+          | Some n when nallargs >= n && nallargs > 0 ->
               let args1, args2 = List.chop n args in
-              let subscopes, impls =
-                match DAst.get f with
-                | GRef (ref,us) ->
-                  let subscopes =
-                    try List.skipn n (find_arguments_scope ref)
-                    with Failure _ -> [] in
-                  let impls =
-                    let impls =
-                      select_impargs_size
-                        (List.length args) (implicits_of_global ref) in
-                    try List.skipn n impls with Failure _ -> [] in
-                  subscopes,impls
-                | _ ->
-                  [], [] in
+              let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
+              let args2impls = try List.skipn n argsimpls with Failure _ -> [] in
+              (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
               (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
-              args2, subscopes, impls
-          | GApp (f, args), None ->
+              args2, args2scopes, args2impls
+          | None when nallargs > 0 ->
             begin match DAst.get f with
-            | GRef (ref,us) ->
-              let subscopes = find_arguments_scope ref in
-              let impls =
-                  select_impargs_size
-                    (List.length args) (implicits_of_global ref) in
-              f, args, subscopes, impls
+            | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
             end
-          | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], []
-          | _, None -> t, [], [], []
+          | Some 0 when nallargs = 0 ->
+            begin match DAst.get f with
+            | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], []
+            | _ -> t, [], [], []
+            end
+          | None -> t, [], [], []
           | _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
           match_notation_constr !print_universes t pat in
         (* Try availability of interpretation ... *)
-        let e =
-          match keyrule with
+        match keyrule with
           | NotationRule (sc,ntn) ->
              (match availability_of_entry_coercion custom (fst ntn) with
              | None -> raise No_match
@@ -1171,22 +1211,25 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
                     List.map (fun (bl,(subentry,(scopt,scl))) ->
                       pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
                       binderlists in
-                  insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key))
+                  let c = make_notation loc ntn (l,ll,bl,bll) in
+                  let c = insert_coercion coercion (insert_delimiters c key) in
+                  let args = fill_arg_scopes args argsscopes allscopes in
+                  let args = extern_args (extern true) vars args in
+                  CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args)
           | SynDefRule kn ->
              match availability_of_entry_coercion custom InConstrEntrySomeLevel with
              | None -> raise No_match
              | Some coercion ->
               let l =
                 List.map (fun (c,(subentry,(scopt,scl))) ->
-                  extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
+                  extern true (subentry,(scopt,scl@snd scopes)) vars c)
                   terms in
-              let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in
-              insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
-        if List.is_empty args then e
-        else
-          let args = fill_arg_scopes args argsscopes allscopes in
-          let args = extern_args (extern true) vars args in
-          CAst.make ?loc @@ explicitize false argsimpls (None,e) args
+              let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in
+              let a = CRef (cf,None) in
+              let args = fill_arg_scopes args argsscopes allscopes in
+              let args = extern_args (extern true) vars args in
+              let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in
+              insert_coercion coercion c
       with
           No_match -> extern_notation allscopes vars t rules
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c699f79351..f4ae5bf676 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1643,7 +1643,7 @@ let drop_notations_pattern looked_for genv =
           | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
           | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-     | CPatCstr (qid, Some expl_pl, pl) ->
+    | CPatCstr (qid, Some expl_pl, pl) ->
       let g = try Nametab.locate qid
               with Not_found ->
               raise (InternalizationError (loc,NotAConstructor qid)) in
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 3e36373b77..cc661aeba3 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -12,7 +12,10 @@
    format *)
 type t = float
 
-let is_nan f = f <> f
+(* The [f : float] type annotation enable the compiler to compile f <> f
+   as comparison on floats rather than the polymorphic OCaml comparison
+   which is much slower. *)
+let is_nan (f : float) = f <> f
 let is_infinity f = f = infinity
 let is_neg_infinity f = f = neg_infinity
 
@@ -42,19 +45,20 @@ let abs = abs_float
 
 type float_comparison = FEq | FLt | FGt | FNotComparable
 
-let eq x y = x = y
+(* See above comment on [is_nan] for the [float] type annotations. *)
+let eq (x : float) (y : float) = x = y
 [@@ocaml.inline always]
 
-let lt x y = x < y
+let lt (x : float) (y : float) = x < y
 [@@ocaml.inline always]
 
-let le x y = x <= y
+let le (x : float) (y : float) = x <= y
 [@@ocaml.inline always]
 
 (* inspired by lib/util.ml; see also #10471 *)
-let pervasives_compare = compare
+let pervasives_compare (x : float) (y : float) = compare x y
 
-let compare x y =
+let compare (x : float) (y : float) =
   if x < y then FLt
   else
   (
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f6f2058c13..e8adde2605 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -321,6 +321,8 @@ let universes_of_private eff =
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
+let structure_body_of_safe_env env = env.revstruct
+
 let sections_of_safe_env senv = senv.sections
 
 let get_section = function
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 92bbd264fa..e6f2fc4a5d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -37,6 +37,8 @@ val env_of_safe_env : safe_environment -> Environ.env
 
 val sections_of_safe_env : safe_environment -> section_data Section.t option
 
+val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
+
 (** The safe_environment state monad *)
 
 type safe_transformer0 = safe_environment -> safe_environment
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2dc3e8a934..853be82eb8 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -26,43 +26,8 @@ open Common
 (*S Part I: computing Coq environment. *)
 (***************************************)
 
-(* FIXME: this is a Libobject hack that should be removed. *)
-module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> (Label.t * structure_field_body) option end)
-
-let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
-| f -> f o
-| exception Not_found -> None
-
 let toplevel_env () =
-  let get_reference = function
-  | (_,kn), Lib.Leaf Libobject.AtomicObject o ->
-    let mp,l = KerName.repr kn in
-    let handler =
-      DynHandle.add Declare.Internal.objConstant begin fun _ ->
-        let constant = Global.lookup_constant (Constant.make1 kn) in
-        Some (l, SFBconst constant)
-      end @@
-      DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
-        let inductive = Global.lookup_mind (MutInd.make1 kn) in
-        Some (l, SFBmind inductive)
-      end @@
-      DynHandle.empty
-    in
-    handle handler o
-    | (_,kn), Lib.Leaf Libobject.ModuleObject _ ->
-      let mp,l = KerName.repr kn in
-      let modl = Global.lookup_module (MPdot (mp, l)) in
-      Some (l, SFBmodule modl)
-    | (_,kn), Lib.Leaf Libobject.ModuleTypeObject _ ->
-      let mp,l = KerName.repr kn in
-      let modtype = Global.lookup_modtype (MPdot (mp, l)) in
-      Some (l, SFBmodtype modtype)
-    | (_,kn), Lib.Leaf Libobject.IncludeObject _ ->
-      user_err Pp.(str "No extraction of toplevel Include yet.")
-    | _ -> None
-  in
-  List.rev (List.map_filter get_reference (Lib.contents ()))
-
+  List.rev (Safe_typing.structure_body_of_safe_env (Global.safe_env ()))
 
 let environment_until dir_opt =
   let rec parse = function
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5ab4409f8b..e2ee5426b5 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -69,18 +69,15 @@ exception FullyUnfocused
 
 let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
-    CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way")
+    Pp.str "This proof is focused, but cannot be unfocused this way"
   | NoSuchGoals (i,j) when Int.equal i j ->
-      CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+    Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-      CErrors.user_err ~hdr:"Focus" Pp.(
-        str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
-      )
+    Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
   | NoSuchGoal id ->
-      CErrors.user_err
-        ~hdr:"Focus"
-        Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
-  | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
+    Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
+  | FullyUnfocused ->
+    Pp.str "The proof is not focused"
   | _ -> raise CErrors.Unhandled
 end
 
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 66e2ae5c29..61e8741973 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -79,7 +79,7 @@ module Strict = struct
       (function
       | FailedBullet (b,sugg) ->
         let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in
-        CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg)
+        Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg)
       | _ -> raise CErrors.Unhandled)
 
 
@@ -204,8 +204,7 @@ exception SuggestNoSuchGoals of int * Proof.t
 let _ = CErrors.register_handler begin function
     | SuggestNoSuchGoals(n,proof) ->
       let suffix = suggest proof in
-      CErrors.user_err
-        Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
-            pr_non_empty_arg (fun x -> x) suffix)
+      Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
+          pr_non_empty_arg (fun x -> x) suffix)
     | _ -> raise CErrors.Unhandled
   end
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 3c9803432a..a4a06873b8 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -27,7 +27,7 @@ let use_unification_heuristics () = !use_unification_heuristics_ref
 
 exception NoSuchGoal
 let () = CErrors.register_handler begin function
-  | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
+  | NoSuchGoal -> Pp.(str "No such goal.")
   | _ -> raise CErrors.Unhandled
 end
 
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
new file mode 100644
index 0000000000..83dd2f40fb
--- /dev/null
+++ b/test-suite/output/Notations5.out
@@ -0,0 +1,248 @@
+p 0 0 true
+     : 0 = 0 /\ true = true
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+p 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p (A:=nat)
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+p (A:=nat)
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@p
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0 0 true
+     : 0 = 0 /\ true = true
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+p
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@p
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+f x true
+     : 0 = 0 /\ true = true
+f x (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+f x (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+@f nat
+     : forall a1 a2 : nat,
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+@f
+     : forall (A : Type) (a1 a2 : A),
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+x.(f) true
+     : 0 = 0 /\ true = true
+x.(f) (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+x.(f) (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+@f nat
+     : forall a1 a2 : nat,
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+@f
+     : forall (A : Type) (a1 a2 : A),
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+p
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+u
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+u
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+u
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+u
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+u
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+u
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+u 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+u 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+@u nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@u nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+u 0 0 true
+     : 0 = 0 /\ true = true
+u 0 0 true
+     : 0 = 0 /\ true = true
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+v 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+v 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+##
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+##
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+##
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+##
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p 0 0 true
+     : 0 = 0 /\ true = true
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
new file mode 100644
index 0000000000..b3bea929ba
--- /dev/null
+++ b/test-suite/output/Notations5.v
@@ -0,0 +1,340 @@
+Module AppliedTermsPrinting.
+
+(* Test different printing paths for applied terms *)
+
+  Module InferredGivenImplicit.
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Check p 0 0 true.
+  (* p 0 0 true *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check p 0.
+  (* p 0 *)
+  Check @p _ 0 0 bool.
+  (* p 0 0 (B:=bool) *)
+  Check p 0 0 (B:=bool).
+  (* p 0 0 (B:=bool) *)
+  Check @p nat.
+  (* p (A:=nat) *)
+  Check p (A:=nat).
+  (* p (A:=nat) *)
+  Check @p _ 0 0.
+  (* @p nat 0 0 *)
+  Check @p.
+  (* @p *)
+
+  Unset Printing Implicit Defensive.
+  Check @p _ 0 0 bool.
+  (* p 0 0 *)
+  Check @p nat.
+  (* p *)
+  Set Printing Implicit Defensive.
+  End InferredGivenImplicit.
+
+  Module ManuallyGivenImplicit.
+  Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b.
+
+  Check p 0 0 true.
+  (* p 0 0 true *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check p 0.
+  (* p 0 *)
+  Check @p _ 0 0 bool.
+  (* p 0 0 *)
+  Check p 0 0 (B:=bool).
+  (* p 0 0 *)
+  Check @p nat.
+  (* p *)
+  Check p (A:=nat).
+  (* p *)
+  Check @p _ 0 0.
+  (* @p nat 0 0 *)
+  Check @p.
+  (* @p *)
+
+  End ManuallyGivenImplicit.
+
+  Module ProjectionWithImplicits.
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Record T {A} (a1 a2:A) := { f : forall B (b:B), a1 = a2 /\ b = b }.
+  Parameter x : T 0 0.
+  Check f x true.
+  (* f x true *)
+  Check @f _ _ _ x bool.
+  (* f x (B:=bool) *)
+  Check f x (B:=bool).
+  (* f x (B:=bool) *)
+  Check @f nat.
+  (* @f nat *)
+  Check @f _ 0 0.
+  (* f (a1:=0) (a2:=0) *)
+  Check f (a1:=0) (a2:=0).
+  (* f (a1:=0) (a2:=0) *)
+  Check @f.
+  (* @f *)
+
+  Unset Printing Implicit Defensive.
+  Check f (a1:=0) (a2:=0).
+  (* f *)
+  Set Printing Implicit Defensive.
+
+  Set Printing Projections.
+
+  Check x.(f) true.
+  (* x.(f) true *)
+  Check x.(@f _ _ _) bool.
+  (* x.(f) (B:=bool) *)
+  Check x.(f) (B:=bool).
+  (* x.(f) (B:=bool) *)
+  Check @f nat.
+  (* @f nat *)
+  Check @f _ 0 0.
+  (* f (a1:=0) (a2:=0) *)
+  Check f (a1:=0) (a2:=0).
+  (* f (a1:=0) (a2:=0) *)
+  Check @f.
+  (* @f *)
+
+  Unset Printing Implicit Defensive.
+  Check f (a1:=0) (a2:=0).
+  (* f *)
+
+  End ProjectionWithImplicits.
+
+  Module AtAbbreviationForApplicationHead.
+
+  Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b.
+
+  Notation u := @p.
+
+  Check u _.
+  (* p *)
+  Check p.
+  (* p *)
+  Check @p.
+  (* u *)
+  Check u.
+  (* u *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check u nat 0 0 bool.
+  (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *)
+  Check u nat 0 0.
+  (* @p nat 0 0 *)
+  Check @p nat 0 0.
+  (* @p nat 0 0 *)
+
+  End AtAbbreviationForApplicationHead.
+
+  Module AbbreviationForApplicationHead.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation u := p.
+
+  Check p.
+  (* u *)
+  Check @p.
+  (* u -- BUG *)
+  Check @u.
+  (* u -- BUG *)
+  Check u.
+  (* u *)
+  Check p 0 0.
+  (* u 0 0 *)
+  Check u 0 0.
+  (* u 0 0 *)
+  Check @p nat 0 0.
+  (* @u nat 0 0 *)
+  Check @u nat 0 0.
+  (* @u nat 0 0 *)
+  Check p 0 0 true.
+  (* u 0 0 true *)
+  Check u 0 0 true.
+  (* u 0 0 true *)
+
+  End AbbreviationForApplicationHead.
+
+  Module AtAbbreviationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation v := (@p _ 0).
+
+  Check v.
+  (* v *)
+  Check p 0 0.
+  (* v 0 *)
+  Check v 0.
+  (* v 0 *)
+  Check v 0 true.
+  (* v 0 (B:=bool) true -- BUG *)
+  Check @p nat 0.
+  (* v *)
+  Check @p nat 0 0.
+  (* @v 0 *)
+  Check @v 0.
+  (* @v 0 *)
+  Check @p nat 0 0 bool.
+  (* v 0 (B:=bool) *)
+
+  End AtAbbreviationForPartialApplication.
+
+  Module AbbreviationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation v := (p 0).
+
+  Check v.
+  (* v *)
+  Check p 0 0.
+  (* v 0 *)
+  Check v 0.
+  (* v 0 *)
+  Check v 0 true.
+  (* v 0 (B:=bool) true -- BUG *)
+  Check @p nat 0.
+  (* v *)
+  Check @p nat 0 0.
+  (* @v 0 *)
+  Check @v 0.
+  (* @v 0 *)
+  Check @p nat 0 0 bool.
+  (* v 0 (B:=bool) *)
+
+  End AbbreviationForPartialApplication.
+
+  Module NotationForHeadApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "##" := p (at level 0).
+
+  Check p.
+  (* ## *)
+  Check ##.
+  (* ## *)
+  Check p 0.
+  (* ## 0 *)
+  Check ## 0.
+  (* ## 0 *)
+  Check p 0 0.
+  (* ## 0 0 *)
+  Check ## 0 0.
+  (* ## 0 0 *)
+  Check p 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check ## 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check p 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+  Check ## 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+
+  End NotationForHeadApplication.
+
+  Module AtNotationForHeadApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "##" := @p (at level 0).
+
+  Check p.
+  (* p *)
+  Check @p.
+  (* ## *)
+  Check ##.
+  (* ## *)
+  Check p 0.
+  (* p 0 -- why not "## nat 0" *)
+  Check ## nat 0.
+  (* p 0 *)
+  Check ## nat 0 0.
+  (* @p nat 0 0 *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check ## nat 0 0 _.
+  (* p 0 0 *)
+  Check ## nat 0 0 bool.
+  (* p 0 0 (B:=bool) *)
+  Check ## nat 0 0 bool true.
+  (* p 0 0 true *)
+
+  End AtNotationForHeadApplication.
+
+  Module NotationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "## q" := (p q) (at level 0, q at level 0).
+
+  Check p 0.
+  (* ## 0 *)
+  Check ## 0.
+  (* ## 0 *)
+  (* Check ## 0 0. *)
+  (* Anomaly *)
+  Check p 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+  Check ## 0 0 bool.
+  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check p 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check ## 0 0 bool true.
+  (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *)
+
+  End NotationForPartialApplication.
+
+  Module AtNotationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "## q" := (@p _ q) (at level 0, q at level 0).
+
+  Check p 0.
+  (* ## 0 *)
+  Check ## 0.
+  (* ## 0 *)
+  (* Check ## 0 0. *)
+  (* Anomaly *)
+  Check p 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+  Check ## 0 0 bool.
+  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check p 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check ## 0 0 bool true.
+  (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *)
+
+  End AtNotationForPartialApplication.
+
+End AppliedTermsPrinting.
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index c81a4abc1b..80b72225f0 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -124,7 +124,7 @@ module Proof_global = struct
   let () =
     CErrors.register_handler begin function
       | NoCurrentProof ->
-        CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
+        Pp.(str "No focused proof (No proof-editing in progress).")
       | _ -> raise CErrors.Unhandled
     end