diff --git a/coq/label_lexico.v b/coq/label_lexico.v
index 03fa8758854887025c07e5541124873e9b582da2..d09563371a5a2a69ef4470ade8aae80ac81261ca 100644
--- a/coq/label_lexico.v
+++ b/coq/label_lexico.v
@@ -331,6 +331,8 @@ Proof.
       try (apply IHs1; auto).
 Qed.
 
+
+Definition custom_label := (string * nat)%type.
 (* Module Type TType. *)
 (*   Parameter T : Type. *)
 (* End TType. *)
diff --git a/ott/base.ott b/ott/base.ott
index 2e18543ed0a8ff6c99b160fbd860466867095a08..132a650fd4cbc3c689cda7c4182a0713d3cc8444 100644
--- a/ott/base.ott
+++ b/ott/base.ott
@@ -8,9 +8,17 @@ grammar
 
 %% Types
 
+user_label  :: 'user_label_' ::= {{coq string}} {{com Label / variable}}
+  | id :: S :: id {{coq [[id]]}} {{ocaml (Aux.explode [[id]])}}
+
+custom_label  :: 'custom_label_' ::= {{coq custom_label}}
+  | id :: S :: id {{coq [[id]]}} {{ocaml (Aux.explode [[id]])}}
+
+
 % We do not distinguish variables from field labels (nor environments from records)
-label, l, var, x :: 'label_' ::= {{coq string}} {{com Label / variable}} 
-  | id :: S :: user {{coq [[id]]}} {{ocaml (Aux.explode [[id]])}}
+label, l, var, x :: 'label_' ::= {{coq string}} {{com Label / variable}}
+  | user_label :: :: user
+  | custom_label :: :: custom
 
 rty :: 'rty_' ::= {{com Record type}}
   | { l_1 : ty_1 ; .. ; l_n : ty_n } :: :: record
@@ -120,7 +128,7 @@ defns
   %   G |- { l_1 : ty_1 ; .. ; l_n : ty_n } @ { l'_1 : ty'_1 ; .. ; l'_m : ty'_m } == { l_1 : ty_1 ; .. ; l_n : ty_n ; l'_1 : ty'_1 ; .. ; l'_m : ty'_m }
 
   % defn
-  %   G |- | ty | :: :: type_canon :: Tcanon_ {{com Canonicity of type}} by 
+  %   G |- | ty | :: :: type_canon :: Tcanon_ {{com Canonicity of type}} by
 
   %   G |- | ty_1 | .. G |- | ty_n |
   %   sorted { l_1 ; .. ; l_n }