4 files changed, 45 insertions, 39 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 681d6ba541..362fe83ffa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1211,9 +1211,14 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
         let (t,args,argsscopes,argsimpls) = match n with
           | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args 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 *)
+              let args2scopes =
+                if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in
+              let args2impls =
+                if n = 0 then
+                  (* Note: NApp(NRef f,[]), hence n=0, encodes @f and
+                     conventionally deactivates implicit arguments *)
+                  []
+                else try List.skipn n argsimpls with Failure _ -> [] in
               DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
           | None ->
             begin match DAst.get f with
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b870fa6f6f..2966c1126d 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,10 +111,11 @@ fun x : option Z => match x with
                     | NONE2 => 0
                     end
      : option Z -> Z
-fun x : list ?T => match x with
-                   | NIL => NONE2
-                   | (_ :') t => SOME2 t
-                   end
+fun x : list ?T =>
+match x with
+| NIL => NONE3 (list ?T)
+| (_ :') t => SOME3 (list ?T) t
+end
      : list ?T -> option (list ?T)
 where
 ?T : [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 9287ea1d4f..990a7151b4 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -78,27 +78,27 @@ f
        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
-u
+u ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-u
+u ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-@u
+u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-@u
+u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u 0 0
+u nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-u 0 0
+u nat 0 0 bool
      : forall b : bool, 0 = 0 /\ b = b
-@u nat 0 0
+u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-@u nat 0 0
+u 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
@@ -196,7 +196,7 @@ where
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-##
+## ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
@@ -204,23 +204,23 @@ where
      : 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
-## 0
+## nat 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-## 0
+## nat 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-@p nat 0 0
+## nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-## 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0
+## nat 0 0 bool
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 true
+## nat 0 0 bool true
      : 0 = 0 /\ true = true
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 81cedc03b4..0b78c388fa 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -115,21 +115,21 @@ Module AppliedTermsPrinting.
   Notation u := @p.
 
   Check u _.
-  (* u -- INCONSISTENT parsing/printing *)
+  (* u ?A *)
   Check p.
-  (* u *)
+  (* u ?A *)
   Check @p.
-  (* @u -- INCONSISTENT parsing/printing *)
+  (* u *)
   Check u.
-  (* @u -- INCONSISTENT parsing/printing *)
+  (* u *)
   Check p 0 0.
-  (* u 0 0 *)
+  (* u nat 0 0 ?B *)
   Check u nat 0 0 bool.
-  (* u 0 0 -- INCONSISTENT parsing/printing *)
+  (* u nat 0 0 bool *)
   Check u nat 0 0.
-  (* @u nat 0 0 *)
+  (* u nat 0 0 *)
   Check @p nat 0 0.
-  (* @u nat 0 0 *)
+  (* u nat 0 0 *)
 
   End AtAbbreviationForApplicationHead.
 
@@ -263,25 +263,25 @@ Module AppliedTermsPrinting.
   Notation "##" := @p (at level 0).
 
   Check p.
-  (* ## -- INCONSISTENT parsing/printing *)
+  (* ## ?A *)
   Check @p.
   (* ## *)
   Check ##.
   (* ## *)
   Check p 0.
-  (* ## 0 *)
+  (* ## nat 0 *)
   Check ## nat 0.
-  (* ## 0 -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 *)
   Check ## nat 0 0.
-  (* @p nat 0 0 *)
+  (* ## nat 0 0 *)
   Check p 0 0.
-  (* ## 0 0 *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 _.
-  (* ## 0 0 -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 bool.
-  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 0 bool *)
   Check ## nat 0 0 bool true.
-  (* ## 0 0 true -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 0 bool true *)
 
   End AtNotationForHeadApplication.