diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index c689848fce291..9790ae77db0ec 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -241,15 +241,33 @@ The term :g:`c (top -> top) (fun x => x) c` infinitely reduces to itself.
 Lack of tactic support
 ----------------------
 
-Some tactics do not handle |SProp| as they were not correctly ported. While in
-most of the cases they will just fail, in some cases this can result in sending
-ill-typed terms to the kernel, which will fail with anomalies at `Qed`.
+Every binder in a term (such as `fun x` or `forall x`) caches
+information called the :gdef:`relevance mark` indicating whether its type is
+in |SProp| or not. This is used to efficiently implement proof
+irrelevance.
+
+Relevance marks are invisible to the user, but code outside the kernel
+may generate incorrect marks resulting in bugs. Typically this means a
+conversion will incorrectly fail as a variable was incorrectly marked
+proof relevant.
 
 .. warn:: Bad relevance
 
   This is a developer warning, which is treated as an error by default. It is
   emitted by the kernel when it is passed a term with incorrect relevance marks.
-  This is always caused by a bug in Coq, which should thus be reported and
+  This is always caused by a bug in Coq (or a plugin), which should thus be reported and
   fixed. In order to allow the user to work around such bugs, we leave the
   ability to unset the ``bad-relevance`` warning for the time being, so that the
   kernel will silently repair the proof term instead of failing.
+
+.. flag:: Printing Relevance Marks
+
+   This :term:`flag` enables debug printing of relevance marks. It is off by default.
+   Note that :flag:`Printing All` does not affect printing of relevance marks.
+
+   .. coqtop:: all
+
+      Set Printing Relevance Marks.
+
+      Check fun x : nat => x.
+      Check fun (P:SProp) (p:P) => p.
diff --git a/interp/constrexpr.mli b/interp/constrexpr.mli
index 6a33325ae892f..98bb72ce64608 100644
--- a/interp/constrexpr.mli
+++ b/interp/constrexpr.mli
@@ -30,6 +30,12 @@ type quality_expr =
   | CQConstant of Sorts.Quality.constant
   | CQualVar of qvar_expr
 
+type relevance_expr =
+  | CRelevant | CIrrelevant
+  | CRelevanceVar of qvar_expr
+
+type relevance_info_expr = relevance_expr option
+
 type sort_expr = (qvar_expr option * (sort_name_expr * int) list) Glob_term.glob_sort_gen
 
 type instance_expr = quality_expr list * univ_level_expr list
@@ -176,11 +182,12 @@ and branch_expr =
   (cases_pattern_expr list list * constr_expr) CAst.t
 
 and fix_expr =
-    lident * recursion_order_expr option *
-      local_binder_expr list * constr_expr * constr_expr
+  lident * relevance_info_expr
+  * recursion_order_expr option *
+  local_binder_expr list * constr_expr * constr_expr
 
 and cofix_expr =
-    lident * local_binder_expr list * constr_expr * constr_expr
+    lident * relevance_info_expr * local_binder_expr list * constr_expr * constr_expr
 
 and recursion_order_expr_r =
   | CStructRec of lident
@@ -190,8 +197,8 @@ and recursion_order_expr = recursion_order_expr_r CAst.t
 
 (* Anonymous defs allowed ?? *)
 and local_binder_expr =
-  | CLocalAssum   of lname list * binder_kind * constr_expr
-  | CLocalDef     of lname * constr_expr * constr_expr option
+  | CLocalAssum   of lname list * relevance_info_expr * binder_kind * constr_expr
+  | CLocalDef     of lname * relevance_info_expr * constr_expr * constr_expr option
   | CLocalPattern of cases_pattern_expr
 
 and constr_notation_substitution =
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index f273eab6b4ad9..bd3ea5c1510bc 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -34,6 +34,13 @@ let qvar_expr_eq c1 c2 = match c1, c2 with
   | CRawQVar q1, CRawQVar q2 -> Sorts.QVar.equal q1 q2
   | (CQVar _ | CQAnon _ | CRawQVar _), _ -> false
 
+let relevance_expr_eq a b = match a, b with
+  | CRelevant, CRelevant | CIrrelevant, CIrrelevant -> true
+  | CRelevanceVar q1, CRelevanceVar q2 -> qvar_expr_eq q1 q2
+  | (CRelevant | CIrrelevant | CRelevanceVar _), _ -> false
+
+let relevance_info_expr_eq = Option.equal relevance_expr_eq
+
 let univ_level_expr_eq u1 u2 =
   Glob_ops.glob_sort_gen_eq sort_name_expr_eq u1 u2
 
@@ -57,10 +64,10 @@ let binder_kind_eq b1 b2 = match b1, b2 with
 let default_binder_kind = Default Explicit
 
 let names_of_local_assums bl =
-  List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl)
+  List.flatten (List.map (function CLocalAssum(l,_,_,_)->l|_->[]) bl)
 
 let names_of_local_binders bl =
-  List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_,_)->[l]|CLocalPattern _ -> assert false) bl)
+  List.flatten (List.map (function CLocalAssum(l,_,_,_)->l|CLocalDef(l,_,_,_)->[l]|CLocalPattern _ -> assert false) bl)
 
 (**********************************************************************)
 (* Functions on constr_expr *)
@@ -150,21 +157,21 @@ module EqGen (A:sig val constr_expr_eq : constr_expr -> constr_expr -> bool end)
   let recursion_order_expr_eq r1 r2 = CAst.eq recursion_order_expr_eq_r r1 r2
 
   let local_binder_eq l1 l2 = match l1, l2 with
-    | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
+    | CLocalDef (n1, _, e1, t1), CLocalDef (n2, _, e2, t2) ->
       CAst.eq Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
-    | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
-      (* Don't care about the [binder_kind] *)
+    | CLocalAssum (n1, _, _, e1), CLocalAssum (n2, _, _, e2) ->
+      (* Don't care about the metadata *)
       List.equal (CAst.eq Name.equal) n1 n2 && constr_expr_eq e1 e2
     | _ -> false
 
-  let fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) =
+  let fix_expr_eq (id1,_,r1,bl1,a1,b1) (id2,_,r2,bl2,a2,b2) =
     (lident_eq id1 id2) &&
     Option.equal recursion_order_expr_eq r1 r2 &&
     List.equal local_binder_eq bl1 bl2 &&
     constr_expr_eq a1 a2 &&
     constr_expr_eq b1 b2
 
-  let cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
+  let cofix_expr_eq (id1,_,bl1,a1,b1) (id2,_,bl2,a2,b2) =
     (lident_eq id1 id2) &&
     List.equal local_binder_eq bl1 bl2 &&
     constr_expr_eq a1 a2 &&
@@ -283,10 +290,10 @@ let constr_loc c = CAst.(c.loc)
 let cases_pattern_expr_loc cp = CAst.(cp.loc)
 
 let local_binder_loc = let open CAst in function
-  | CLocalAssum ({ loc } ::_,_,t)
-  | CLocalDef ( { loc },t,None) -> Loc.merge_opt loc (constr_loc t)
-  | CLocalDef ( { loc },b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
-  | CLocalAssum ([],_,_) -> assert false
+  | CLocalAssum ({ loc } ::_,_,_,t)
+  | CLocalDef ( { loc },_,t,None) -> Loc.merge_opt loc (constr_loc t)
+  | CLocalDef ( { loc },_,b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
+  | CLocalAssum ([],_,_,_) -> assert false
   | CLocalPattern { loc } -> loc
 
 let local_binders_loc bll = match bll with
@@ -340,11 +347,11 @@ let ids_of_cases_tomatch tms =
     tms Id.Set.empty
 
 let rec fold_local_binders g f n acc b = let open CAst in function
-  | CLocalAssum (nal,bk,t)::l ->
+  | CLocalAssum (nal,_,bk,t)::l ->
     let nal = List.(map (fun {v} -> v) nal) in
     let n' = List.fold_right (Name.fold_right g) nal n in
     f n (fold_local_binders g f n' acc b l) t
-  | CLocalDef ( { v = na },c,t)::l ->
+  | CLocalDef ( { v = na },_,c,t)::l ->
     Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
   | CLocalPattern pat :: l ->
     let n, acc = cases_pattern_fold_names g (f n) (n,acc) pat in
@@ -383,8 +390,8 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
       Option.fold_left
         (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
     | CFix (_,l) ->
-      let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in
-      List.fold_right (fun (_,ro,lb,t,c) acc ->
+      let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_,_) -> g id) l n in
+      List.fold_right (fun (_,_,ro,lb,t,c) acc ->
           fold_local_binders g f n'
             (fold_local_binders g f n acc t lb) c lb) l acc
     | CCoFix (_,_) ->
@@ -452,10 +459,10 @@ let fold_map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
   let open CAst in
   let h (e,bl) = function
-      CLocalAssum(nal,k,ty) ->
-      (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
-    | CLocalDef( { loc ; v = na } as cna ,c,ty) ->
-      (Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl)
+      CLocalAssum(nal,r,k,ty) ->
+      (map_binder g e nal, CLocalAssum(nal,r,k,f e ty)::bl)
+    | CLocalDef( { loc ; v = na } as cna ,r,c,ty) ->
+      (Name.fold_right g na e, CLocalDef(cna,r,f e c,Option.map (f e) ty)::bl)
     | CLocalPattern pat ->
       let e, pat = fold_map_cases_pattern g f e pat in
       (e, CLocalPattern pat::bl) in
@@ -497,20 +504,20 @@ let map_constr_expr_with_binders g f e = CAst.map (function
       let e' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
       CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
     | CFix (id,dl) ->
-      CFix (id,List.map (fun (id,n,bl,t,d) ->
+      CFix (id,List.map (fun (id,r,n,bl,t,d) ->
           let (e',bl') = fold_map_local_binders f g e bl in
           let t' = f e' t in
           (* Note: fix names should be inserted before the arguments... *)
-          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
+          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
-          (id,n,bl',t',d')) dl)
+          (id,r,n,bl',t',d')) dl)
     | CCoFix (id,dl) ->
-      CCoFix (id,List.map (fun (id,bl,t,d) ->
+      CCoFix (id,List.map (fun (id,r,bl,t,d) ->
           let (e',bl') = fold_map_local_binders f g e bl in
           let t' = f e' t in
-          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
+          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
-          (id,bl',t',d')) dl)
+          (id,r,bl',t',d')) dl)
     | CArray (u, t, def, ty) ->
       CArray (u, Array.map (f e) t, f e def, f e ty)
     | CHole _ | CGenarg _ | CGenargGlob _ | CEvar _ | CPatVar _ | CSort _
@@ -563,7 +570,7 @@ let split_at_annot bl na =
     end
   | Some { loc; v = id } ->
     let rec aux acc = function
-      | CLocalAssum (bls, k, t) as x :: rest ->
+      | CLocalAssum (bls, rinfo, k, t) as x :: rest ->
         let test { CAst.v = na } = match na with
           | Name id' -> Id.equal id id'
           | Anonymous -> false
@@ -574,11 +581,11 @@ let split_at_annot bl na =
           | _ ->
             let ans = match l with
               | [] -> acc
-              | _ -> CLocalAssum (l, k, t) :: acc
+              | _ -> CLocalAssum (l, rinfo, k, t) :: acc
             in
-            (List.rev ans, CLocalAssum (r, k, t) :: rest)
+            (List.rev ans, CLocalAssum (r, rinfo, k, t) :: rest)
         end
-      | CLocalDef ({ CAst.v = na },_,_) as x :: rest ->
+      | CLocalDef ({ CAst.v = na },_,_,_) as x :: rest ->
         if Name.equal (Name id) na then
           CErrors.user_err ?loc
             (Id.print id ++ str" must be a proper parameter and not a local definition.")
@@ -596,9 +603,9 @@ let split_at_annot bl na =
 let mkIdentC id   = CAst.make @@ CRef (qualid_of_ident id,None)
 let mkRefC r      = CAst.make @@ CRef (r,None)
 let mkCastC (a,k,t) = CAst.make @@ CCast (a,k,t)
-let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
+let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,None,bk,a)],b)
 let mkLetInC  (id,a,t,b)   = CAst.make @@ CLetIn (id,a,t,b)
-let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,bk,a)],b)
+let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,None,bk,a)],b)
 
 let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 9daa6817d185c..b1ca478591106 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -19,6 +19,7 @@ open Constrexpr
 val sort_name_expr_eq : sort_name_expr -> sort_name_expr -> bool
 val univ_level_expr_eq : univ_level_expr -> univ_level_expr -> bool
 val sort_expr_eq : sort_expr -> sort_expr -> bool
+val relevance_info_expr_eq : relevance_info_expr -> relevance_info_expr -> bool
 
 val explicitation_eq : explicitation -> explicitation -> bool
 (** Equality on [explicitation]. *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 24bb70cf7561d..2d545f776612d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -773,7 +773,7 @@ let rec flatten_application c = match DAst.get c with
 
 let same_binder_type ty nal c =
   match nal, DAst.get c with
-  | _::_, (GProd (_,_,ty',_) | GLambda (_,_,ty',_)) -> glob_constr_eq ty ty'
+  | _::_, (GProd (_,_,_,ty',_) | GLambda (_,_,_,ty',_)) -> glob_constr_eq ty ty'
   | [], _ -> true
   | _ -> assert false
 
@@ -814,13 +814,13 @@ let extern_prim_token_delimiter_if_required n key_n scope_n scopes =
 (* mapping decl                                                       *)
 
 let extended_glob_local_binder_of_decl loc = function
-  | (p,bk,None,t) -> GLocalAssum (p,bk,t)
-  | (p,bk,Some x, t) ->
+  | (p,r,bk,None,t) -> GLocalAssum (p,r,bk,t)
+  | (p,r,bk,Some x, t) ->
     assert (bk = Explicit);
     match DAst.get t with
-    | GHole (GNamedHole _) -> GLocalDef (p,x,Some t)
-    | GHole _ -> GLocalDef (p,x,None)
-    | _ -> GLocalDef (p,x,Some t)
+    | GHole (GNamedHole _) -> GLocalDef (p,r,x,Some t)
+    | GHole _ -> GLocalDef (p,r,x,None)
+    | _ -> GLocalDef (p,r,x,Some t)
 
 let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u)
 
@@ -862,19 +862,26 @@ let extern_glob_sort_name uvars = function
       | None -> CRawType u
     end
 
-let extern_glob_qvar uvars = function
+let extern_glob_qvar = function
   | GLocalQVar {v=Anonymous;loc} -> CQAnon loc
   | GLocalQVar {v=Name id; loc} -> CQVar (qualid_of_ident ?loc id)
   | GRawQVar q -> CRawQVar q
   | GQVar q -> CRawQVar q
 
-let extern_glob_quality uvars = function
+let extern_relevance = function
+  | GRelevant -> CRelevant
+  | GIrrelevant -> CIrrelevant
+  | GRelevanceVar q -> CRelevanceVar (extern_glob_qvar q)
+
+let extern_relevance_info = Option.map extern_relevance
+
+let extern_glob_quality = function
   | GQConstant q -> CQConstant q
-  | GQualVar q -> CQualVar (extern_glob_qvar uvars q)
+  | GQualVar q -> CQualVar (extern_glob_qvar q)
 
 let extern_glob_sort uvars u =
   let map (q, l) =
-    Option.map (extern_glob_qvar uvars) q, List.map (on_fst (extern_glob_sort_name uvars)) l
+    Option.map extern_glob_qvar q, List.map (on_fst (extern_glob_sort_name uvars)) l
   in
   map_glob_sort_gen map u
 
@@ -887,7 +894,7 @@ let extern_glob_sort uvars = function
 
 let extern_instance uvars = function
   | Some (ql,ul) when !print_universes ->
-    let ql = List.map (extern_glob_quality uvars) ql in
+    let ql = List.map extern_glob_quality ql in
     let ul = List.map (map_glob_sort_gen (extern_glob_sort_name uvars)) ul in
     Some (ql,ul)
   | _ -> None
@@ -904,8 +911,8 @@ let rec insert_impargs impargs r = match impargs with
   | [] -> r
   | bk :: rest ->
     match DAst.get r with
-    | GProd (na,_,t,c) ->
-      DAst.make ?loc:r.loc (GProd (na, bk, t, insert_impargs rest c))
+    | GProd (na,rinfo,_,t,c) ->
+      DAst.make ?loc:r.loc (GProd (na, rinfo, bk, t, insert_impargs rest c))
     | _ -> r
 
 let rec extern inctx ?impargs scopes vars r =
@@ -985,16 +992,17 @@ let rec extern inctx ?impargs scopes vars r =
   | GProj (f,params,c) ->
       extern_applied_proj inctx scopes vars f params c []
 
-  | GLetIn (na,b,t,c) ->
-      CLetIn (make ?loc na,sub_extern (Option.has_some t) scopes vars b,
-              Option.map (extern_typ scopes vars) t,
-              extern inctx ?impargs scopes (add_vname vars na) c)
+  | GLetIn (na,_,b,t,c) ->
+    CLetIn (make ?loc na,
+            sub_extern (Option.has_some t) scopes vars b,
+            Option.map (extern_typ scopes vars) t,
+            extern inctx ?impargs scopes (add_vname vars na) c)
 
-  | GProd (na,bk,t,c) ->
-      factorize_prod ?impargs scopes vars na bk t c
+  | GProd (na,r,bk,t,c) ->
+      factorize_prod ?impargs scopes vars na r bk t c
 
-  | GLambda (na,bk,t,c) ->
-      factorize_lambda inctx scopes vars na bk t c
+  | GLambda (na,r,bk,t,c) ->
+      factorize_lambda inctx scopes vars na r bk t c
 
   | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
@@ -1058,7 +1066,7 @@ let rec extern inctx ?impargs scopes vars r =
                    | None -> None
                    | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x)))
                              in
-                 ((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
+                 ((CAst.make fi), None, n, bl, extern_typ scopes vars0 ty,
                   sub_extern true scopes vars1 def)) idv
              in
              CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
@@ -1069,7 +1077,7 @@ let rec extern inctx ?impargs scopes vars r =
                  let (_,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in
                  let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in
-                 ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
+                 ((CAst.make fi),None,bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern true scopes vars1 bv.(i))) idv
              in
              CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
@@ -1103,8 +1111,9 @@ and extern_typ ?impargs (subentry,(_,scopes)) =
 
 and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,([],scopes))
 
-and factorize_prod ?impargs scopes vars na bk t c =
+and factorize_prod ?impargs scopes vars na r bk t c =
   let implicit_type = is_reserved_type na t in
+  let r = extern_relevance_info r in
   let aty = extern_typ scopes vars t in
   let vars = add_vname vars na in
   let store, get = set_temporary_memory () in
@@ -1131,21 +1140,23 @@ and factorize_prod ?impargs scopes vars na bk t c =
       let bk = Option.default Explicit impargs_hd in
       let c' = extern_typ ?impargs:impargs_tl scopes vars c in
       match na, c'.v with
-      | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
-           when binding_kind_eq bk bk'
-                && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *)
-                && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
-         let ty = if implicit_type then ty else aty in
-         CProdN (CLocalAssum(make na::nal,Default bk,ty)::bl,b)
+      | Name id, CProdN (CLocalAssum(nal,r',Default bk',ty)::bl,b)
+        when relevance_info_expr_eq r r'
+            && binding_kind_eq bk bk'
+            && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *)
+            && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
+        let ty = if implicit_type then ty else aty in
+        CProdN (CLocalAssum(make na::nal,r,Default bk,ty)::bl,b)
       | _, CProdN (bl,b) ->
          let ty = if implicit_type then hole else aty in
-         CProdN (CLocalAssum([make na],Default bk,ty)::bl,b)
+         CProdN (CLocalAssum([make na],r,Default bk,ty)::bl,b)
       | _, _ ->
          let ty = if implicit_type then hole else aty in
-         CProdN ([CLocalAssum([make na],Default bk,ty)],c')
+         CProdN ([CLocalAssum([make na],r,Default bk,ty)],c')
 
-and factorize_lambda inctx scopes vars na bk t c =
+and factorize_lambda inctx scopes vars na r bk t c =
   let implicit_type = is_reserved_type na t in
+  let r = extern_relevance_info r in
   let aty = extern_typ scopes vars t in
   let vars = add_vname vars na in
   let store, get = set_temporary_memory () in
@@ -1166,44 +1177,45 @@ and factorize_lambda inctx scopes vars na bk t c =
   | _, _ ->
       let c' = sub_extern inctx scopes vars c in
       match c'.v with
-      | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b)
-           when binding_kind_eq bk bk'
-                && not (occur_name na ty)  (* avoid na in ty escapes scope *)
-                && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
-         let aty = if implicit_type then ty else aty in
-         CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
+      | CLambdaN (CLocalAssum(nal,r',Default bk',ty)::bl,b)
+        when relevance_info_expr_eq r r'
+          && binding_kind_eq bk bk'
+          && not (occur_name na ty)  (* avoid na in ty escapes scope *)
+          && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
+        let aty = if implicit_type then ty else aty in
+        CLambdaN (CLocalAssum(make na::nal,r,Default bk,aty)::bl,b)
       | CLambdaN (bl,b) ->
          let ty = if implicit_type then hole else aty in
-         CLambdaN (CLocalAssum([make na],Default bk,ty)::bl,b)
+         CLambdaN (CLocalAssum([make na],r,Default bk,ty)::bl,b)
       | _ ->
          let ty = if implicit_type then hole else aty in
-         CLambdaN ([CLocalAssum([make na],Default bk,ty)],c')
+         CLambdaN ([CLocalAssum([make na],r,Default bk,ty)],c')
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
   | b :: l ->
     match DAst.get b with
-    | GLocalDef (na,bd,ty) ->
+    | GLocalDef (na,r,bd,ty) ->
       let (assums,ids,l) =
         extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l in
       (assums,na::ids,
-       CLocalDef(CAst.make na, extern false scopes vars bd,
+       CLocalDef(CAst.make na, extern_relevance_info r, extern false scopes vars bd,
                    Option.map (extern_typ scopes vars) ty) :: l)
 
-    | GLocalAssum (na,bk,ty) ->
+    | GLocalAssum (na,r,bk,ty) ->
       let implicit_type = is_reserved_type na ty in
       let ty = extern_typ scopes vars ty in
       (match extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l with
-          (assums,ids,CLocalAssum(nal,k,ty')::l)
-            when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) &&
+       | (assums,ids,CLocalAssum(nal,r',k,ty')::l)
+         when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) &&
               match na with Name id -> not (occur_var_constr_expr id ty')
-                | _ -> true ->
-              (na::assums,na::ids,
-               CLocalAssum(CAst.make na::nal,k,ty')::l)
-        | (assums,ids,l) ->
-            let ty = if implicit_type then hole else ty in
-            (na::assums,na::ids,
-             CLocalAssum([CAst.make na],Default bk,ty) :: l))
+                          | _ -> true ->
+         (na::assums,na::ids,
+          CLocalAssum(CAst.make na::nal,r',k,ty')::l)
+       | (assums,ids,l) ->
+         let ty = if implicit_type then hole else ty in
+         (na::assums,na::ids,
+          CLocalAssum([CAst.make na],extern_relevance_info r,Default bk,ty) :: l))
 
     | GLocalPattern ((p,_),_,bk,ty) ->
       let ty =
@@ -1448,16 +1460,16 @@ let rec glob_of_pat
   | PProd (na,t,c) ->
       let na',avoid' = compute_displayed_name_in_pattern (Global.env ()) sigma avoid na c in
       let env' = Termops.add_name na' env in
-      GProd (na',Explicit,glob_of_pat avoid env sigma t,glob_of_pat avoid' env' sigma c)
+      GProd (na',None,Explicit,glob_of_pat avoid env sigma t,glob_of_pat avoid' env' sigma c)
   | PLetIn (na,b,t,c) ->
       let na',avoid' = Namegen.compute_displayed_let_name_in (Global.env ()) sigma Namegen.RenamingForGoal avoid na in
       let env' = Termops.add_name na' env in
-      GLetIn (na',glob_of_pat avoid env sigma b, Option.map (glob_of_pat avoid env sigma) t,
+      GLetIn (na',None,glob_of_pat avoid env sigma b, Option.map (glob_of_pat avoid env sigma) t,
               glob_of_pat avoid' env' sigma c)
   | PLambda (na,t,c) ->
       let na',avoid' = compute_displayed_name_in_pattern (Global.env ()) sigma avoid na c in
       let env' = Termops.add_name na' env in
-      GLambda (na',Explicit,glob_of_pat avoid env sigma t, glob_of_pat avoid' env' sigma c)
+      GLambda (na',None,Explicit,glob_of_pat avoid env sigma t, glob_of_pat avoid' env' sigma c)
   | PIf (c,b1,b2) ->
       GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
            glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 166d800d679a1..67c0dabc0a8d0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -336,8 +336,8 @@ let set_env_scopes env (scopt,subscopes) =
 let env_for_pattern env =
   {pat_scopes = (env.tmp_scope, env.scopes); pat_ids = Some env.ids}
 
-let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, bk, t, body)
-let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
+let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, None, bk, t, body)
+let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, None, bk, t, body)
 
 (**********************************************************************)
 (* Utilities for binders                                              *)
@@ -370,23 +370,23 @@ let build_impls ?loc n bk na acc =
 
 let impls_binder_list =
   let rec aux acc n = function
-    | (na,bk,None,_) :: binders -> aux (build_impls n bk na acc) (n+1) binders
-    | (na,bk,Some _,_) :: binders -> aux acc n binders
+    | (na,_,bk,None,_) :: binders -> aux (build_impls n bk na acc) (n+1) binders
+    | (na,_,bk,Some _,_) :: binders -> aux acc n binders
     | [] -> (n,acc)
   in aux []
 
 let impls_type_list n ?(args = []) =
   let rec aux acc n c = match DAst.get c with
-    | GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
+    | GProd (na,_,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
     | _ -> List.rev acc
   in aux args n
 
 let impls_term_list n ?(args = []) =
   let rec aux acc n c = match DAst.get c with
-    | GLambda (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
+    | GLambda (na,_,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
     | GRec (fix_kind, nas, args, tys, bds) ->
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
-       let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in
+       let n,acc' = List.fold_left (fun (n,acc) (na, _, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in
        aux acc' n bds.(nb)
     |_ -> List.rev acc
   in aux args n
@@ -508,7 +508,7 @@ let push_name_env ntnvars implargs env =
       pure_push_name_env (id,(Variable,implargs,[],uid),Id.Map.mem id ntnvars) env
 
 let remember_binders_impargs env bl =
-  List.map_filter (fun (na,_,_,_) ->
+  List.map_filter (fun (na,_,_,_,_) ->
       match na with
       | Anonymous -> None
       | Name id -> Some (id,Id.Map.find id env.impls,Id.Set.mem id env.ntn_binding_ids)) bl
@@ -581,11 +581,11 @@ let intern_assumption intern ntnvars env nal bk ty =
      env, b
 
 let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
-  | GLocalAssum (na,bk,t) -> (na,bk,None,t)
-  | GLocalDef (na,c,Some t) -> (na,Explicit,Some c,t)
-  | GLocalDef (na,c,None) ->
+  | GLocalAssum (na,r,bk,t) -> (na,None,bk,None,t)
+  | GLocalDef (na,r,c,Some t) -> (na,None,Explicit,Some c,t)
+  | GLocalDef (na,r,c,None) ->
       let t = DAst.make ?loc @@ GHole (GBinderType na) in
-      (na,Explicit,Some c,t)
+      (na,None,Explicit,Some c,t)
   | GLocalPattern (_,_,_,_) ->
       Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed here")
   )
@@ -624,13 +624,13 @@ let intern_cases_pattern_as_binder intern test_kind ntnvars env bk (CAst.{v=p;lo
   env,((disjpat,il),id),bk,t
 
 let intern_local_binder_aux intern ntnvars (env,bl) = function
-  | CLocalAssum(nal,bk,ty) ->
+  | CLocalAssum(nal,_,bk,ty) ->
       let env, bl' = intern_assumption intern ntnvars env nal bk ty in
-      let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
+      let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,None,c,t)) bl' in
       env, bl' @ bl
-  | CLocalDef( {loc; v=na} as locna,def,ty) ->
+  | CLocalDef( {loc; v=na} as locna,_,def,ty) ->
      let env,(na,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in
-     env, (DAst.make ?loc @@ GLocalDef (na,def,ty)) :: bl
+     env, (DAst.make ?loc @@ GLocalDef (na,None,def,ty)) :: bl
   | CLocalPattern p ->
       let env, ((disjpat,il),id),bk,t = intern_cases_pattern_as_binder intern test_kind_tolerant ntnvars env Explicit p in
       (env, (DAst.make ?loc:p.CAst.loc @@ GLocalPattern((disjpat,il),id,bk,t)) :: bl)
@@ -654,11 +654,11 @@ let intern_generalization intern env ntnvars loc bk c =
         if pi then
           (fun {loc=loc';v=id} acc ->
             DAst.make ?loc:(Loc.merge_opt loc' loc) @@
-            GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (GBinderType (Name id)), acc))
+            GProd (Name id, None, bk, DAst.make ?loc:loc' @@ GHole (GBinderType (Name id)), acc))
         else
           (fun {loc=loc';v=id} acc ->
             DAst.make ?loc:(Loc.merge_opt loc' loc) @@
-            GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (GBinderType (Name id)), acc))
+            GLambda (Name id, None, bk, DAst.make ?loc:loc' @@ GHole (GBinderType (Name id)), acc))
     in
       List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
         let env' = push_name_env ntnvars [] env CAst.(make @@ Name id) in
@@ -670,9 +670,9 @@ let rec expand_binders ?loc mk bl c =
   | [] -> c
   | b :: bl ->
      match DAst.get b with
-     | GLocalDef (n, b, oty) ->
-        expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, b, oty, c))
-     | GLocalAssum (n, bk, t) ->
+     | GLocalDef (n, r, b, oty) ->
+        expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, r, b, oty, c))
+     | GLocalAssum (n, _, bk, t) ->
         expand_binders ?loc mk bl (mk ?loc (n,bk,t) c)
      | GLocalPattern ((disjpat,ids), id, bk, ty) ->
         let tm = DAst.make ?loc (GVar id) in
@@ -752,8 +752,8 @@ let cook_pattern ((disjpat, ids), id) =
 
 let extract_pattern_from_binder b =
   match DAst.get b with
-  | GLocalDef (n, b, oty) -> user_err ?loc:b.CAst.loc (str "Local definitions not supported here.")
-  | GLocalAssum (na, bk, t) -> None, na, bk, t
+  | GLocalDef _ -> user_err ?loc:b.CAst.loc (str "Local definitions not supported here.")
+  | GLocalAssum (na, _, bk, t) -> None, na, bk, t
   | GLocalPattern (patl, id, bk, ty) ->
     let pat, na = cook_pattern (patl, id) in
     pat, na, bk, ty
@@ -826,10 +826,10 @@ let terms_of_binders bl =
     | bnd :: l ->
       let loc = bnd.loc in
       begin match DAst.get bnd with
-      | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l
-      | GLocalDef (Name id,_,_) -> extract_variables l
-      | GLocalDef (Anonymous,_,_)
-      | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
+      | GLocalAssum (Name id,_,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l
+      | GLocalDef (Name id,_,_,_) -> extract_variables l
+      | GLocalDef (Anonymous,_,_,_)
+      | GLocalAssum (Anonymous,_,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
       | GLocalPattern (([u],_),_,_,_) -> term_of_pat u :: extract_variables l
       | GLocalPattern ((_,_),_,_,_) -> error_cannot_coerce_disjunctive_pattern_term ?loc ()
       end
@@ -843,13 +843,13 @@ let flatten_generalized_binders_if_any y l =
      (* if l has more than one element, this means we had a generalized binder *)
      let select_iter a =
        match DAst.get a with
-       | GLocalAssum (Name id,_,_) when Id.equal id ldots_var -> AddNList
+       | GLocalAssum (Name id,_,_,_) when Id.equal id ldots_var -> AddNList
        | _ -> AddBinderIter (y,a) in
      List.map select_iter l
 
 let flatten_binders bl =
   let dispatch = function
-    | CLocalAssum (nal,bk,t) -> List.map (fun na -> CLocalAssum ([na],bk,t)) nal
+    | CLocalAssum (nal,r,bk,t) -> List.map (fun na -> CLocalAssum ([na],r,bk,t)) nal
     | a -> [a] in
   List.flatten (List.map dispatch bl)
 
@@ -891,7 +891,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
            aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter
         | AddLetIn (na,c,t)::rest,terminator,iter ->
            let env,(na,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in
-           DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter)))
+           DAst.make ?loc (GLetIn (na,None,c,t,aux_letin env (rest,terminator,iter)))
         | AddNList::rest,terminator,iter ->
            DAst.make ?loc (GApp (DAst.make ?loc (GVar ldots_var), [aux_letin env (rest,terminator,iter)]))
         in
@@ -961,7 +961,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
         let bl = flatten_binders bl in
         let bl = if revert then List.rev bl else bl in
         (* We isolate let-ins which do not contribute to the repeated pattern *)
-        let l = List.map (function | CLocalDef (na,c,t) -> AddLetIn (na,c,t)
+        let l = List.map (function | CLocalDef (na,_,c,t) -> AddLetIn (na,c,t)
                                    | binder -> AddPreBinderIter (y,binder)) bl in
         (* We stack the binders to iterate or let-ins to insert *)
         aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var)
@@ -2152,7 +2152,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           apply_impargs env loc c []
 
     | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
-        let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
+        let lf = List.map (fun ({CAst.v = id},_,_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
         let n =
           try List.index0 Id.equal iddef lf
@@ -2163,7 +2163,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         in
         let env = restart_lambda_binders env in
         let idl_temp = Array.map
-            (fun (id,recarg,bl,ty,_) ->
+            (fun (id,_,recarg,bl,ty,_) ->
                let recarg = Option.map (function { CAst.v = v; loc } -> match v with
                  | CStructRec i -> i
                  | _ -> user_err ?loc Pp.(str "Well-founded induction requires Program Fixpoint or Function.")) recarg
@@ -2171,7 +2171,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in
                let bl = List.rev_map glob_local_binder_of_extended bl in
                let n = Option.map (fun recarg ->
-                   List.fold_left_until (fun n (id,_,body,_) -> match body with
+                   List.fold_left_until (fun n (id,_,_,body,_) -> match body with
                        | None ->
                          if Name.equal id (Name recarg.v) then Stop n else Cont (n+1)
                        | Some _ -> Cont n (* let-ins don't count *))
@@ -2186,7 +2186,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
            let binder_index,fix_args = impls_binder_list 1 bli in
            let impls = impls_type_list ~args:fix_args binder_index tyi in
            push_name_env ntnvars impls en (CAst.make @@ Name name)) 0 env lf in
-        let idl = Array.map2 (fun (_,_,_,_,bd) (n,bl,ty,before_impls) ->
+        let idl = Array.map2 (fun (_,_,_,_,_,bd) (n,bl,ty,before_impls) ->
             (* We add the binders common to body and type to the environment *)
             let env_body = restore_binders_impargs env_rec before_impls in
             (n,bl,ty,intern {env_body with tmp_scope = []} bd)) dl idl_temp in
@@ -2199,7 +2199,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
               Array.map (fun (_,_,_,bd) -> bd) idl)
 
     | CCoFix ({ CAst.loc = locid; v = iddef }, dl) ->
-        let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in
+        let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
         let n =
           try List.index0 Id.equal iddef lf
@@ -2210,7 +2210,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         in
         let env = restart_lambda_binders env in
         let idl_tmp = Array.map
-          (fun ({ CAst.loc; v = id },bl,ty,_) ->
+          (fun ({ CAst.loc; v = id },_,bl,ty,_) ->
             let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
             let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
             let bl_impls = remember_binders_impargs env' bl in
@@ -2220,7 +2220,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           let binder_index,cofix_args = impls_binder_list 1 bli in
           push_name_env ntnvars (impls_type_list ~args:cofix_args binder_index tyi)
             en (CAst.make @@ Name name)) 0 env lf in
-        let idl = Array.map2 (fun (_,_,_,bd) (b,c,bl_impls) ->
+        let idl = Array.map2 (fun (_,_,_,_,bd) (b,c,bl_impls) ->
           (* We add the binders common to body and type to the environment *)
           let env_body = restore_binders_impargs env_rec bl_impls in
           (b,c,intern {env_body with tmp_scope = []} bd)) dl idl_tmp in
@@ -2242,7 +2242,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         let inc1 = intern_restart_binders (reset_tmp_scope env) c1 in
         let int = Option.map (intern_type_restart_binders env) t in
         DAst.make ?loc @@
-        GLetIn (na.CAst.v, inc1, int,
+        GLetIn (na.CAst.v, None, inc1, int,
           intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
     | CNotation (_,(InConstrEntry,"- _"), ([a],[],[],[])) when is_non_zero a ->
       let p = match a.CAst.v with CPrim (Number (_, p)) -> p | _ -> assert false in
@@ -2844,7 +2844,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma bl =
   let flags = { Pretyping.all_no_fail_flags with program_mode } in
   let env, sigma, par, impls =
     List.fold_left
-      (fun (env,sigma,params,impls) (na, k, b, t) ->
+      (fun (env,sigma,params,impls) (na, _, k, b, t) ->
        let t' =
          if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
          else t
@@ -2892,7 +2892,7 @@ let interp_named_context_evars ?(program_mode=false) ?(impl_env=empty_internaliz
       (fun (int_env, acc) b ->
         let int_env, bl = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (int_env,[]) b in
         let bl = List.map glob_local_binder_of_extended bl in
-        let acc = List.fold_right (fun (na, bk, b, t) (int_env, (env,sigma,params,impls)) ->
+        let acc = List.fold_right (fun (na, _, bk, b, t) (int_env, (env,sigma,params,impls)) ->
           let id = match na with
           | Name id -> id
           | Anonymous -> user_err Pp.(str "Unexpected anonymous variable.")
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 941f35a89996b..7f6643aabec45 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -213,7 +213,7 @@ let implicits_of_glob_constr ?(with_products=true) l =
   in
   let rec aux c =
     match DAst.get c with
-    | GProd (na, bk, t, b) ->
+    | GProd (na, _, bk, t, b) ->
       if with_products then add_impl na bk (aux b)
       else
         let () = match bk with
@@ -221,11 +221,11 @@ let implicits_of_glob_constr ?(with_products=true) l =
           | MaxImplicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
           | Explicit -> ()
         in []
-    | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
-    | GLetIn (na, b, t, c) -> aux c
+    | GLambda (na, _, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
+    | GLetIn (na, _, b, t, c) -> aux c
     | GRec (fix_kind, nas, args, tys, bds) ->
       let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
-      List.fold_right (fun (na,bk,t,_) l ->
+      List.fold_right (fun (na,_,bk,t,_) l ->
           match t with
           | Some _ -> l
           | _ -> add_impl ?loc:c.CAst.loc na bk l)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index a7212b85d9e6a..b4c82ea555c0e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -409,18 +409,18 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
       let e = h.switch_lambda e in
       let ty = Option.map (f (h.restart_prod e)) ty in
       let e',disjpat,na',bk,ty = g e na ty in
-      GLambda (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+      GLambda (na',None,bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NProd (na,ty,c) ->
       let e = h.switch_prod e in
       let ty = Option.map (f (h.restart_prod e)) ty in
       let e',disjpat,na',bk,ty = g e na ty in
-      GProd (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+      GProd (na',None,bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NLetIn (na,b,t,c) ->
       let t = Option.map (f (h.restart_prod e)) t in
       let e',disjpat,na,bk,t = g e na t in
       test_implicit_argument_mark bk;
       (match disjpat with
-       | None -> GLetIn (na,f (h.restart_lambda e) b,t,f e' c)
+       | None -> GLetIn (na,None, f (h.restart_lambda e) b,t,f e' c)
        | Some (disjpat,_id) -> test_pattern_cast t; DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
   | NCases (sty,rtntypopt,tml,eqnl) ->
       let e = h.no e in
@@ -458,7 +458,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
       let e = h.no e in
       let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
           let e,na = protect g e na in
-          (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
+          (e,(na,None,Explicit,Option.map (f e) oc,f e b)))) e dll in
       let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
       GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | NCast (c,k,t) -> GCast (f e c, k, f (h.slide e) t)
@@ -671,9 +671,9 @@ let notation_constr_and_vars_of_glob_constr recvars a =
      (* Treat applicative notes as binary nodes *)
      let a,args = List.sep_last args in mkNApp1 (aux (DAst.make (GApp (g, args))), aux a)
   | GProj (p,args,c) -> NProj (p, List.map aux args, aux c)
-  | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux_type ty,aux c)
-  | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux_type ty,aux c)
-  | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
+  | GLambda (na,_,bk,ty,c) -> add_name found na; NLambda (na,aux_type ty,aux c)
+  | GProd (na,_,bk,ty,c) -> add_name found na; NProd (na,aux_type ty,aux c)
+  | GLetIn (na,_,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
   | GCases (sty,rtntypopt,tml,eqnl) ->
       let f {CAst.v=(idl,pat,rhs)} = List.iter (add_id found) idl; (pat,aux rhs) in
       NCases (sty,Option.map aux rtntypopt,
@@ -692,7 +692,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
       NIf (aux c,(na,Option.map aux po),aux b1,aux b2)
   | GRec (fk,idl,dll,tl,bl) ->
       Array.iter (add_id found) idl;
-      let dll = Array.map (List.map (fun (na,bk,oc,b) ->
+      let dll = Array.map (List.map (fun (na,_,bk,oc,b) ->
          if bk != Explicit then
            user_err Pp.(str "Binders marked as implicit not allowed in notations.");
          add_name found na; (na,Option.map aux oc,aux b))) dll in
@@ -950,7 +950,7 @@ let abstract_return_type_context pi mklam tml rtno =
 let abstract_return_type_context_glob_constr tml rtn =
   abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal)
     (fun na c -> DAst.make @@
-      GLambda(na,Explicit,DAst.make @@ GHole (GInternalHole), c)) tml rtn
+      GLambda(na,None,Explicit,DAst.make @@ GHole (GInternalHole), c)) tml rtn
 
 let abstract_return_type_context_notation_constr tml rtn =
   abstract_return_type_context snd
@@ -965,9 +965,9 @@ let rec push_context_binders vars = function
   | [] -> vars
   | b :: bl ->
     let vars = match DAst.get b with
-    | GLocalAssum (na,_,_) -> Termops.add_vname vars na
+    | GLocalAssum (na,_,_,_) -> Termops.add_vname vars na
     | GLocalPattern ((disjpat,ids),p,bk,t) -> List.fold_right Id.Set.add ids vars
-    | GLocalDef (na,_,_) -> Termops.add_vname vars na in
+    | GLocalDef (na,_,_,_) -> Termops.add_vname vars na in
     push_context_binders vars bl
 
 let is_term_meta id metas =
@@ -1119,15 +1119,27 @@ let unify_opt_term alp v v' =
 
 let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match
 
+let unify_relevance_info r r' = if relevance_info_eq r r' then r else raise No_match
+
 let unify_binder_upto alp b b' =
   let loc, loc' = CAst.(b.loc, b'.loc) in
   match DAst.get b, DAst.get b' with
-  | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
+  | GLocalAssum (na,r,bk,t), GLocalAssum (na',r',bk',t') ->
      let alp, na = unify_name_upto alp na na' in
-     alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp.renaming t t')
-  | GLocalDef (na,c,t), GLocalDef (na',c',t') ->
+     alp, DAst.make ?loc @@
+     GLocalAssum
+       (na,
+        unify_relevance_info r r',
+        unify_binding_kind bk bk',
+        unify_term alp.renaming t t')
+  | GLocalDef (na,r,c,t), GLocalDef (na',r',c',t') ->
      let alp, na = unify_name_upto alp na na' in
-     alp, DAst.make ?loc @@ GLocalDef (na, unify_term alp.renaming c c', unify_opt_term alp.renaming t t')
+     alp, DAst.make ?loc @@
+     GLocalDef
+       (na,
+        unify_relevance_info r r',
+        unify_term alp.renaming c c',
+        unify_opt_term alp.renaming t t')
   | GLocalPattern ((disjpat,ids),id,bk,t), GLocalPattern ((disjpat',_),_,bk',t') when List.length disjpat = List.length disjpat' ->
      let alp, p = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in
      alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp.renaming t t')
@@ -1160,8 +1172,8 @@ let unify_pat renaming p p' =
 
 let unify_term_binder renaming c = DAst.(map (fun b' ->
   match DAst.get c, b' with
-  | GVar id, GLocalAssum (na', bk', t') ->
-     GLocalAssum (unify_id renaming id na', bk', t')
+  | GVar id, GLocalAssum (na', r', bk', t') ->
+     GLocalAssum (unify_id renaming id na', r', bk', t')
   | _, GLocalPattern (([p'],ids), id, bk', t') ->
      let p = pat_binder_of_term c in
      GLocalPattern (([unify_pat renaming p p'],ids), id, bk', t')
@@ -1172,7 +1184,7 @@ let rec unify_terms_binders renaming cl bl' =
   | [], [] -> []
   | c :: cl, b' :: bl' ->
      begin match DAst.get b' with
-     | GLocalDef (_, _, t) -> unify_terms_binders renaming cl bl'
+     | GLocalDef (_, _, _, t) -> unify_terms_binders renaming cl bl'
      | _ -> unify_term_binder renaming c b' :: unify_terms_binders renaming cl bl'
      end
   | _ -> raise No_match
@@ -1320,7 +1332,7 @@ let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1
       bind_binding_env alp sigma id2 [pat1]
   | PatVar id1, PatVar (Name id2) when is_onlybindinglist_meta id2 metas ->
       let t1 = DAst.make @@ GHole(GBinderType id1) in
-      bind_bindinglist_env alp sigma id2 [DAst.make @@ GLocalAssum (id1,Explicit,t1)]
+      bind_bindinglist_env alp sigma id2 [DAst.make @@ GLocalAssum (id1,None,Explicit,t1)]
   | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta false id2 metas ->
       bind_binding_env alp sigma id2 [pat1]
   | _, PatVar (Name id2) when is_onlybindinglist_meta id2 metas ->
@@ -1373,8 +1385,8 @@ let match_binderlist match_iter_fun match_termin_fun alp metas sigma rest x y it
       aux false alp' sigma (b::bl) rest
     with No_match ->
     match DAst.get rest with
-    | GLetIn (na,c,t,rest') when glue_inner_letin_with_decls ->
-       let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,c,t) in
+    | GLetIn (na,r,c,t,rest') when glue_inner_letin_with_decls ->
+       let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,r,c,t) in
        (* collect let-in *)
        (try aux true alp sigma (b::bl) rest'
         with OnlyTrailingLetIns
@@ -1488,15 +1500,15 @@ let rec match_ inner u alp metas sigma a1 a2 =
          List.length l1 = List.length l2 + 1 ->
         List.fold_left2 (match_in u alp metas) sigma l1 (l2@[a2])
      | _ -> raise No_match)
-  | GLambda (na1,bk1,t1,b1), NLambda (na2,t2,b2) ->
+  | GLambda (na1,_,bk1,t1,b1), NLambda (na2,t2,b2) ->
      match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
-  | GProd (na1,bk1,t1,b1), NProd (na2,t2,b2) ->
+  | GProd (na1,_,bk1,t1,b1), NProd (na2,t2,b2) ->
      match_extended_binders (not inner) u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
-  | GLetIn (na1,b1,t1,c1), NLetIn (na2,b2,None,c2)
-  | GLetIn (na1,b1,(None as t1),c1), NLetIn (na2,b2,_,c2) ->
+  | GLetIn (na1,_,b1,t1,c1), NLetIn (na2,b2,None,c2)
+  | GLetIn (na1,_,b1,(None as t1),c1), NLetIn (na2,b2,_,c2) ->
      let t = match t1 with Some t -> t | None -> DAst.make @@ GHole(GBinderType na1) in
      match_extended_binders false u alp metas na1 na2 Explicit t (match_in u alp metas sigma b1 b2) c1 c2
-  | GLetIn (na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) ->
+  | GLetIn (na1,_,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) ->
      match_extended_binders false u alp metas na1 na2 Explicit t1
        (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2
   | GCases (sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
@@ -1533,7 +1545,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
         Array.for_all2 (fun l1 l2 -> Int.equal (List.length l1) (List.length l2)) dll1 dll2
         ->
       let alp,sigma = Array.fold_left2
-        (List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) ->
+        (List.fold_left2 (fun (alp,sigma) (na1,_,_,oc1,b1) (na2,oc2,b2) ->
           let sigma =
             match_in u alp metas
               (match_opt (match_in u alp metas) sigma oc1 oc2) b1 b2
@@ -1574,7 +1586,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       | _ -> assert false in
       let (alp,sigma) =
         if is_bindinglist_meta id metas then
-          bind_bindinglist_env alp sigma id [DAst.make @@ GLocalAssum (Name id',Explicit,t1)]
+          bind_bindinglist_env alp sigma id [DAst.make @@ GLocalAssum (Name id',None,Explicit,t1)]
         else
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp a1 [DAst.make @@ GVar id']) b2
@@ -1628,7 +1640,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
      | _ -> assert false)
   | _, _, Name id when is_bindinglist_meta id metas ->
       if (isprod && na1 = Anonymous) then raise No_match (* prefer using "A -> B" for anonymous forall *);
-      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t)] in
+      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,None,bk,t)] in
       match_in u alp metas sigma b1 b2
   | _, _, _ ->
      let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
@@ -1682,10 +1694,10 @@ let group_by_type ids (terms,termlists,binders,binderlists) =
        let v = List.map (fun pat -> match DAst.get pat with
            | GLocalPattern ((disjpat,_),_,_,_) ->
              List.map (glob_constr_of_cases_pattern (Global.env())) disjpat
-           | GLocalAssum (Anonymous,bk,t) ->
+           | GLocalAssum (Anonymous,_,bk,t) ->
              let hole = DAst.make (GHole (GBinderType Anonymous)) in
              [DAst.make (GCast (hole, Some DEFAULTcast, t))]
-           | GLocalAssum (Name id,bk,t) ->
+           | GLocalAssum (Name id,_,bk,t) ->
              [DAst.make (GCast (DAst.make (GVar id), Some DEFAULTcast, t))]
            | GLocalDef _ -> raise No_match) patl in
        (terms',((vars,List.flatten v),scl)::termlists',binders',binderlists')
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index a6bf799b51a09..f7b209295986b 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -28,7 +28,7 @@ open Pcoq.Constr
 let ldots_var = Id.of_string ".."
 
 let binder_of_name expl { CAst.loc = loc; v = na } =
-  CLocalAssum ([CAst.make ?loc na], Default expl,
+  CLocalAssum ([CAst.make ?loc na], None, Default expl,
     CAst.make ?loc @@ CHole (Some (GBinderType na)))
 
 let binders_of_names l =
@@ -257,11 +257,11 @@ GRAMMAR EXTEND Gram
           CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
                  Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
       | "let"; "fix"; fx = fix_decl; "in"; c = term LEVEL "200" ->
-        { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_ as dcl)} = fx in
+        { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_,_ as dcl)} = fx in
           let fix = CAst.make ?loc:locf @@ CFix (lid,[dcl]) in
           CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fix,None,c) }
       | "let"; "cofix"; fx = cofix_body; "in"; c = term LEVEL "200" ->
-        { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_ as dcl)} = fx in
+        { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_ as dcl)} = fx in
           let cofix = CAst.make ?loc:locf @@ CCoFix (lid,[dcl]) in
           CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,cofix,None,c) }
       | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ];
@@ -327,24 +327,24 @@ GRAMMAR EXTEND Gram
       | id = global -> { Global id } ] ]
   ;
   fix_decls:
-    [ [ dcl = fix_decl -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
+    [ [ dcl = fix_decl -> { let (id,_,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
       | dcl = fix_decl; "with"; dcls = LIST1 fix_decl SEP "with"; "for"; id = identref ->
         { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
   ;
   cofix_decls:
-    [ [ dcl = cofix_body -> { let (id,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
+    [ [ dcl = cofix_body -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
       | dcl = cofix_body; "with"; dcls = LIST1 cofix_body SEP "with"; "for"; id = identref ->
         { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
   ;
   fix_decl:
     [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":=";
         c = term LEVEL "200" ->
-        { CAst.make ~loc (id,snd bl,fst bl,ty,c) } ] ]
+        { CAst.make ~loc (id,None,snd bl,fst bl,ty,c) } ] ]
   ;
   cofix_body:
     [ [ id = identref; bl = binders; ty = type_cstr; ":=";
         c = term LEVEL "200" ->
-        { CAst.make ~loc (id,bl,ty,c) } ] ]
+        { CAst.make ~loc (id,None,bl,ty,c) } ] ]
   ;
   term_match:
     [ [ "match"; ci = LIST1 case_item SEP ","; ty = OPT case_type; "with";
@@ -433,13 +433,13 @@ GRAMMAR EXTEND Gram
     (* Same as binders but parentheses around a closed binder are optional if
        the latter is unique *)
     [ [ id = name; idl = LIST0 name; ":"; c = lconstr ->
-        { [CLocalAssum (id::idl,Default Explicit,c)] }
+        { [CLocalAssum (id::idl,None,Default Explicit,c)] }
         (* binders factorized with open binder *)
       | id = name; idl = LIST0 name; bl = binders ->
         { binders_of_names (id::idl) @ bl }
       | id1 = name; ".."; id2 = name ->
         { [CLocalAssum ([id1;(CAst.make ~loc (Name ldots_var));id2],
-                        Default Explicit, CAst.make ~loc @@ CHole (None))] }
+                        None, Default Explicit, CAst.make ~loc @@ CHole (None))] }
       | bl = closed_binder; bl' = binders ->
         { bl@bl' } ] ]
   ;
@@ -447,42 +447,42 @@ GRAMMAR EXTEND Gram
     [ [ l = LIST0 binder -> { List.flatten l } ] ]
   ;
   binder:
-    [ [ id = name -> { [CLocalAssum ([id],Default Explicit, CAst.make ~loc @@ CHole (None))] }
+    [ [ id = name -> { [CLocalAssum ([id], None, Default Explicit, CAst.make ~loc @@ CHole (None))] }
       | bl = closed_binder -> { bl } ] ]
   ;
   closed_binder:
     [ [ "("; id = name; idl = LIST1 name; ":"; c = lconstr; ")" ->
-        { [CLocalAssum (id::idl,Default Explicit,c)] }
+        { [CLocalAssum (id::idl,None,Default Explicit,c)] }
       | "("; id = name; ":"; c = lconstr; ")" ->
-        { [CLocalAssum ([id],Default Explicit,c)] }
+        { [CLocalAssum ([id],None,Default Explicit,c)] }
       | "("; id = name; ":="; c = lconstr; ")" ->
         { match c.CAst.v with
-          | CCast(c, Some DEFAULTcast, t) -> [CLocalDef (id,c,Some t)]
-          | _ -> [CLocalDef (id,c,None)] }
+          | CCast(c, Some DEFAULTcast, t) -> [CLocalDef (id,None,c,Some t)]
+          | _ -> [CLocalDef (id,None,c,None)] }
       | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" ->
-        { [CLocalDef (id,c,Some t)] }
+        { [CLocalDef (id,None,c,Some t)] }
       | "{"; id = name; "}" ->
-        { [CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None))] }
+        { [CLocalAssum ([id], None, Default MaxImplicit, CAst.make ~loc @@ CHole (None))] }
       | "{"; id = name; idl = LIST1 name; ":"; c = lconstr; "}" ->
-        { [CLocalAssum (id::idl,Default MaxImplicit,c)] }
+        { [CLocalAssum (id::idl,None,Default MaxImplicit,c)] }
       | "{"; id = name; ":"; c = lconstr; "}" ->
-        { [CLocalAssum ([id],Default MaxImplicit,c)] }
+        { [CLocalAssum ([id],None,Default MaxImplicit,c)] }
       | "{"; id = name; idl = LIST1 name; "}" ->
-        { List.map (fun id -> CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None))) (id::idl) }
+        { List.map (fun id -> CLocalAssum ([id], None, Default MaxImplicit, CAst.make ~loc @@ CHole (None))) (id::idl) }
       | "["; id = name; "]" ->
-        { [CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None))] }
+        { [CLocalAssum ([id], None, Default NonMaxImplicit, CAst.make ~loc @@ CHole (None))] }
       | "["; id = name; idl = LIST1 name; ":"; c = lconstr; "]" ->
-        { [CLocalAssum (id::idl,Default NonMaxImplicit,c)] }
+        { [CLocalAssum (id::idl,None,Default NonMaxImplicit,c)] }
       | "["; id = name; ":"; c = lconstr; "]" ->
-        { [CLocalAssum ([id],Default NonMaxImplicit,c)] }
+        { [CLocalAssum ([id],None, Default NonMaxImplicit,c)] }
       | "["; id = name; idl = LIST1 name; "]" ->
-        { List.map (fun id -> CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None))) (id::idl) }
+        { List.map (fun id -> CLocalAssum ([id], None, Default NonMaxImplicit, CAst.make ~loc @@ CHole (None))) (id::idl) }
       | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
-        { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc }
+        { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (Explicit, b), t)) tc }
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
-        { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc }
+        { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (MaxImplicit, b), t)) tc }
       | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
-        { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc }
+        { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (NonMaxImplicit, b), t)) tc }
       | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] } ] ]
   ;
   one_open_binder:
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 0b05d83e08b4a..e3138ab39933c 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -22,9 +22,9 @@ let observe_tac s =
 *)
 let rec abstract_glob_constr c = function
   | [] -> c
-  | Constrexpr.CLocalDef (x, b, t) :: bl ->
+  | Constrexpr.CLocalDef (x, _, b, t) :: bl ->
     Constrexpr_ops.mkLetInC (x, b, t, abstract_glob_constr c bl)
-  | Constrexpr.CLocalAssum (idl, k, t) :: bl ->
+  | Constrexpr.CLocalAssum (idl, _, k, t) :: bl ->
     List.fold_right
       (fun x b -> Constrexpr_ops.mkLambdaC ([x], k, t, b))
       idl
@@ -89,10 +89,10 @@ let is_rec names =
     | GRec _ -> CErrors.user_err (Pp.str "GRec not handled")
     | GIf (b, _, lhs, rhs) ->
       lookup names b || lookup names lhs || lookup names rhs
-    | GProd (na, _, t, b) | GLambda (na, _, t, b) ->
+    | GProd (na, _, _, t, b) | GLambda (na, _, _, t, b) ->
       lookup names t
       || lookup (Nameops.Name.fold_right Id.Set.remove na names) b
-    | GLetIn (na, b, t, c) ->
+    | GLetIn (na, _, b, t, c) ->
       lookup names b
       || Option.cata (lookup names) true t
       || lookup (Nameops.Name.fold_right Id.Set.remove na names) c
@@ -119,9 +119,9 @@ let rec rebuild_bl aux bl typ =
   let open Constrexpr in
   match (bl, typ) with
   | [], _ -> (List.rev aux, typ)
-  | CLocalAssum (nal, bk, _) :: bl', typ -> rebuild_nal aux bk bl' nal typ
-  | CLocalDef (na, _, _) :: bl', {CAst.v = CLetIn (_, nat, ty, typ')} ->
-    rebuild_bl (Constrexpr.CLocalDef (na, nat, ty) :: aux) bl' typ'
+  | CLocalAssum (nal, _, bk, _) :: bl', typ -> rebuild_nal aux bk bl' nal typ
+  | CLocalDef (na, _, _, _) :: bl', {CAst.v = CLetIn (_, nat, ty, typ')} ->
+    rebuild_bl (Constrexpr.CLocalDef (na, None, nat, ty) :: aux) bl' typ'
   | _ -> assert false
 
 and rebuild_nal aux bk bl' nal typ =
@@ -130,19 +130,19 @@ and rebuild_nal aux bk bl' nal typ =
   | _, {CAst.v = CProdN ([], typ)} -> rebuild_nal aux bk bl' nal typ
   | [], _ -> rebuild_bl aux bl' typ
   | ( na :: nal
-    , {CAst.v = CProdN (CLocalAssum (na' :: nal', bk', nal't) :: rest, typ')} )
+    , {CAst.v = CProdN (CLocalAssum (na' :: nal', _, bk', nal't) :: rest, typ')} )
     ->
     if Name.equal na.CAst.v na'.CAst.v || Name.is_anonymous na'.CAst.v then
-      let assum = CLocalAssum ([na], bk, nal't) in
+      let assum = CLocalAssum ([na], None, bk, nal't) in
       let new_rest =
-        if nal' = [] then rest else CLocalAssum (nal', bk', nal't) :: rest
+        if nal' = [] then rest else CLocalAssum (nal', None, bk', nal't) :: rest
       in
       rebuild_nal (assum :: aux) bk bl' nal
         (CAst.make @@ CProdN (new_rest, typ'))
     else
-      let assum = CLocalAssum ([na'], bk, nal't) in
+      let assum = CLocalAssum ([na'], None, bk, nal't) in
       let new_rest =
-        if nal' = [] then rest else CLocalAssum (nal', bk', nal't) :: rest
+        if nal' = [] then rest else CLocalAssum (nal', None, bk', nal't) :: rest
       in
       rebuild_nal (assum :: aux) bk bl' (na :: nal)
         (CAst.make @@ CProdN (new_rest, typ'))
@@ -184,7 +184,7 @@ let rec local_binders_length = function
   (* Assume that no `{ ... } contexts occur *)
   | [] -> 0
   | Constrexpr.CLocalDef _ :: bl -> 1 + local_binders_length bl
-  | Constrexpr.CLocalAssum (idl, _, _) :: bl ->
+  | Constrexpr.CLocalAssum (idl, _, _, _) :: bl ->
     List.length idl + local_binders_length bl
   | Constrexpr.CLocalPattern _ :: bl -> assert false
 
@@ -1682,14 +1682,14 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt
     match wf_arg with
     | None -> (
       match args with
-      | [Constrexpr.CLocalAssum ([{CAst.v = Name x}], _k, t)] -> (t, x)
+      | [Constrexpr.CLocalAssum ([{CAst.v = Name x}], _, _k, t)] -> (t, x)
       | _ -> CErrors.user_err (Pp.str "Recursive argument must be specified") )
     | Some wf_args -> (
       try
         match
           List.find
             (function
-              | Constrexpr.CLocalAssum (l, _k, t) ->
+              | Constrexpr.CLocalAssum (l, _, _k, t) ->
                 List.exists
                   (function
                     | {CAst.v = Name id} -> Id.equal id wf_args | _ -> false)
@@ -1697,7 +1697,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt
               | _ -> false)
             args
         with
-        | Constrexpr.CLocalAssum (_, _k, t) -> (t, wf_args)
+        | Constrexpr.CLocalAssum (_, _, _k, t) -> (t, wf_args)
         | _ -> assert false
       with Not_found -> assert false )
   in
@@ -1916,14 +1916,14 @@ let rec chop_n_arrow n t =
         let new_n =
           let rec aux (n : int) = function
             | [] -> n
-            | CLocalAssum (nal, k, t'') :: nal_ta' ->
+            | CLocalAssum (nal, _, k, t'') :: nal_ta' ->
               let nal_l = List.length nal in
               if n >= nal_l then aux (n - nal_l) nal_ta'
               else
                 let new_t' =
                   CAst.make
                   @@ Constrexpr.CProdN
-                       ( CLocalAssum (snd (List.chop n nal), k, t'') :: nal_ta'
+                       ( CLocalAssum (snd (List.chop n nal), None, k, t'') :: nal_ta'
                        , t' )
                 in
                 raise (Stop new_t')
@@ -1948,11 +1948,11 @@ let rec add_args id new_args =
       CProdN
         ( List.map
             (function
-              | CLocalAssum (nal, k, b2) ->
-                CLocalAssum (nal, k, add_args id new_args b2)
-              | CLocalDef (na, b1, t) ->
+              | CLocalAssum (nal, r, k, b2) ->
+                CLocalAssum (nal, r, k, add_args id new_args b2)
+              | CLocalDef (na, r, b1, t) ->
                 CLocalDef
-                  ( na
+                  ( na, r
                   , add_args id new_args b1
                   , Option.map (add_args id new_args) t )
               | CLocalPattern _ ->
@@ -1963,11 +1963,11 @@ let rec add_args id new_args =
       CLambdaN
         ( List.map
             (function
-              | CLocalAssum (nal, k, b2) ->
-                CLocalAssum (nal, k, add_args id new_args b2)
-              | CLocalDef (na, b1, t) ->
+              | CLocalAssum (nal, r, k, b2) ->
+                CLocalAssum (nal, r, k, add_args id new_args b2)
+              | CLocalDef (na, r, b1, t) ->
                 CLocalDef
-                  ( na
+                  ( na, r
                   , add_args id new_args b1
                   , Option.map (add_args id new_args) t )
               | CLocalPattern _ ->
@@ -2034,7 +2034,7 @@ let rec get_args b t :
     * Constrexpr.constr_expr =
   let open Constrexpr in
   match b.CAst.v with
-  | Constrexpr.CLambdaN ((CLocalAssum (nal, k, ta) as d) :: rest, b') ->
+  | Constrexpr.CLambdaN ((CLocalAssum (nal, _, k, ta) as d) :: rest, b') ->
     let n = List.length nal in
     let nal_tas, b'', t'' =
       get_args
@@ -2077,7 +2077,7 @@ let make_graph (f_ref : GlobRef.t) =
       | Constrexpr.CFix (l_id, fixexprl) ->
         let l =
           List.map
-            (fun (id, recexp, bl, t, b) ->
+            (fun (id, _, recexp, bl, t, b) ->
               let {CAst.loc; v = rec_id} =
                 match Option.get recexp with
                 | {CAst.v = CStructRec id} -> id
@@ -2088,8 +2088,8 @@ let make_graph (f_ref : GlobRef.t) =
                 List.flatten
                   (List.map
                      (function
-                       | Constrexpr.CLocalDef (na, _, _) -> []
-                       | Constrexpr.CLocalAssum (nal, _, _) ->
+                       | Constrexpr.CLocalDef (na, _, _, _) -> []
+                       | Constrexpr.CLocalAssum (nal, _, _, _) ->
                          List.map
                            (fun {CAst.loc; v = n} ->
                              CAst.make ?loc
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 362e79dd01ca5..651cf6721b0ce 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -490,7 +490,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
           DAst.make
           @@
           match DAst.get t with
-          | GLambda (na, _, nat, b) -> GLetIn (na, u, None, aux b l)
+          | GLambda (na, _, _, nat, b) -> GLetIn (na, None, u, None, aux b l)
           | _ -> GApp (t, l) )
       in
       build_entry_lc env sigma funnames avoid (aux f args)
@@ -536,7 +536,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
             args_res.result }
     | GApp _ ->
       assert false (* we have collected all the app in [glob_decompose_app] *)
-    | GLetIn (n, v, t, b) ->
+    | GLetIn (n, _, v, t, b) ->
       (* if we have [(let x := v in b) t1 ... tn] ,
          we discard our work and compute the list of constructor for
          [let x = v in (b t1 ... tn)] up to alpha conversion
@@ -590,7 +590,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
               let c, params = List.sep_last args_res.value in
               {args_res with value = DAst.make (GProj (f, params, c))})
             args_res.result }
-  | GLambda (n, _, t, b) ->
+  | GLambda (n, _, _, t, b) ->
     (* we first compute the list of constructor
        corresponding to the body of the function,
        then the one corresponding to the type
@@ -605,7 +605,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
     let new_env = raw_push_named (new_n, None, t) env in
     let b_res = build_entry_lc new_env sigma funnames avoid b in
     combine_results (combine_lam new_n) t_res b_res
-  | GProd (n, _, t, b) ->
+  | GProd (n, _, _, t, b) ->
     (* we first compute the list of constructor
        corresponding to the body of the function,
        then the one corresponding to the type
@@ -617,7 +617,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
     if List.length t_res.result = 1 && List.length b_res.result = 1 then
       combine_results (combine_prod2 n) t_res b_res
     else combine_results (combine_prod n) t_res b_res
-  | GLetIn (n, v, typ, b) ->
+  | GLetIn (n, _, v, typ, b) ->
     (* we first compute the list of constructor
        corresponding to the body of the function,
        then the one corresponding to the value [t]
@@ -906,7 +906,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
   let open Context.Rel.Declaration in
   let open CAst in
   match DAst.get rt with
-  | GProd (n, k, t, b) -> (
+  | GProd (n, _, k, t, b) -> (
     let not_free_in_t id = not (is_free_in id t) in
     let new_crossed_types = t :: crossed_types in
     match DAst.get t with
@@ -1103,7 +1103,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
         (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
       | _ -> (mkGProd (n, t, new_b), Id.Set.filter not_free_in_t id_to_exclude)
       ) )
-  | GLambda (n, k, t, b) -> (
+  | GLambda (n, _, k, t, b) -> (
     let not_free_in_t id = not (is_free_in id t) in
     let new_crossed_types = t :: crossed_types in
     observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt);
@@ -1121,12 +1121,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
       if Id.Set.mem id id_to_exclude && depth >= nb_args then
         (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
       else
-        ( DAst.make @@ GProd (n, k, t, new_b)
+        ( DAst.make @@ GProd (n, None, k, t, new_b)
         , Id.Set.filter not_free_in_t id_to_exclude )
     | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
     (* We have renamed all the anonymous functions during alpha_renaming phase *)
     )
-  | GLetIn (n, v, t, b) -> (
+  | GLetIn (n, _, v, t, b) -> (
     let t =
       match t with
       | None -> v
@@ -1150,7 +1150,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
       (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
     | _ ->
-      ( DAst.make @@ GLetIn (n, t, None, new_b)
+      ( DAst.make @@ GLetIn (n, None, t, None, new_b)
       , (* HOPING IT WOULD WORK *)
         Id.Set.filter not_free_in_t id_to_exclude ) )
   | GLetTuple (nal, (na, rto), t, b) ->
@@ -1201,10 +1201,10 @@ let rec compute_cst_params relnames params gt =
         | _ -> List.fold_left (compute_cst_params relnames) params (f :: args) )
       | GProj (f, args, c) ->
         List.fold_left (compute_cst_params relnames) params (args @ [c])
-      | GLambda (_, _, t, b) | GProd (_, _, t, b) | GLetTuple (_, _, t, b) ->
+      | GLambda (_, _, _, t, b) | GProd (_, _, _, t, b) | GLetTuple (_, _, t, b) ->
         let t_params = compute_cst_params relnames params t in
         compute_cst_params relnames t_params b
-      | GLetIn (_, v, t, b) ->
+      | GLetIn (_, _, v, t, b) ->
         let v_params = compute_cst_params relnames params v in
         let t_params =
           Option.fold_left (compute_cst_params relnames) v_params t
@@ -1271,7 +1271,7 @@ let rec rebuild_return_type rt =
     CAst.make ?loc
     @@ Constrexpr.CProdN
          ( [ Constrexpr.CLocalAssum
-               ([CAst.make Anonymous], Constrexpr.Default Explicit, rt) ]
+               ([CAst.make Anonymous], None, Constrexpr.Default Explicit, rt) ]
          , CAst.make @@ Constrexpr.CSort (UAnonymous {rigid=UnivRigid}) )
 
 let do_build_inductive evd (funconstants : pconstant list)
@@ -1350,6 +1350,7 @@ let do_build_inductive evd (funconstants : pconstant list)
             @@ Constrexpr.CProdN
                  ( [ Constrexpr.CLocalAssum
                        ( [CAst.make n]
+                       , None
                        , Constrexpr_ops.default_binder_kind
                        , with_full_print
                            Constrextern.(extern_glob_constr empty_extern_env)
@@ -1439,6 +1440,7 @@ let do_build_inductive evd (funconstants : pconstant list)
           @@ Constrexpr.CProdN
                ( [ Constrexpr.CLocalAssum
                      ( [CAst.make n]
+                     , None
                      , Constrexpr_ops.default_binder_kind
                      , with_full_print
                          Constrextern.(extern_glob_constr empty_extern_env)
@@ -1465,6 +1467,7 @@ let do_build_inductive evd (funconstants : pconstant list)
         | Some typ ->
           Constrexpr.CLocalDef
             ( CAst.make n
+            , None
             , Constrextern.(extern_glob_constr empty_extern_env) t
             , Some
                 (with_full_print
@@ -1473,6 +1476,7 @@ let do_build_inductive evd (funconstants : pconstant list)
         | None ->
           Constrexpr.CLocalAssum
             ( [CAst.make n]
+            , None
             , Constrexpr_ops.default_binder_kind
             , Constrextern.(extern_glob_constr empty_extern_env) t ))
       rels_params
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index a7f4fdcdd7c10..16f5bf4898bee 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -21,9 +21,9 @@ open Names
 let mkGRef ref = DAst.make @@ GRef (ref, None)
 let mkGVar id = DAst.make @@ GVar id
 let mkGApp (rt, rtl) = DAst.make @@ GApp (rt, rtl)
-let mkGLambda (n, t, b) = DAst.make @@ GLambda (n, Explicit, t, b)
-let mkGProd (n, t, b) = DAst.make @@ GProd (n, Explicit, t, b)
-let mkGLetIn (n, b, t, c) = DAst.make @@ GLetIn (n, b, t, c)
+let mkGLambda (n, t, b) = DAst.make @@ GLambda (n, None, Explicit, t, b)
+let mkGProd (n, t, b) = DAst.make @@ GProd (n, None, Explicit, t, b)
+let mkGLetIn (n, b, t, c) = DAst.make @@ GLetIn (n, None, b, t, c)
 let mkGCases (rto, l, brl) = DAst.make @@ GCases (RegularStyle, rto, l, brl)
 
 let mkGHole () =
@@ -66,21 +66,22 @@ let change_vars =
           GApp (change_vars mapping rt', List.map (change_vars mapping) rtl)
         | GProj (f, rtl, rt) ->
           GProj (f, List.map (change_vars mapping) rtl, change_vars mapping rt)
-        | GLambda (name, k, t, b) ->
+        | GLambda (name, r, k, t, b) ->
           GLambda
             ( name
-            , k
+            , r, k
             , change_vars mapping t
             , change_vars (remove_name_from_mapping mapping name) b )
-        | GProd (name, k, t, b) ->
+        | GProd (name, r, k, t, b) ->
           GProd
             ( name
-            , k
+            , r, k
             , change_vars mapping t
             , change_vars (remove_name_from_mapping mapping name) b )
-        | GLetIn (name, def, typ, b) ->
+        | GLetIn (name, r, def, typ, b) ->
           GLetIn
             ( name
+            , r
             , change_vars mapping def
             , Option.map (change_vars mapping) typ
             , change_vars (remove_name_from_mapping mapping name) b )
@@ -190,24 +191,24 @@ let rec alpha_rt excluded rt =
     @@
     match DAst.get rt with
     | (GRef _ | GVar _ | GEvar _ | GPatVar _) as rt -> rt
-    | GLambda (Anonymous, k, t, b) ->
+    | GLambda (Anonymous, r, k, t, b) ->
       let new_id =
         Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded)
       in
       let new_excluded = new_id :: excluded in
       let new_t = alpha_rt new_excluded t in
       let new_b = alpha_rt new_excluded b in
-      GLambda (Name new_id, k, new_t, new_b)
-    | GProd (Anonymous, k, t, b) ->
+      GLambda (Name new_id, r, k, new_t, new_b)
+    | GProd (Anonymous, r, k, t, b) ->
       let new_t = alpha_rt excluded t in
       let new_b = alpha_rt excluded b in
-      GProd (Anonymous, k, new_t, new_b)
-    | GLetIn (Anonymous, b, t, c) ->
+      GProd (Anonymous, r, k, new_t, new_b)
+    | GLetIn (Anonymous, r, b, t, c) ->
       let new_b = alpha_rt excluded b in
       let new_t = Option.map (alpha_rt excluded) t in
       let new_c = alpha_rt excluded c in
-      GLetIn (Anonymous, new_b, new_t, new_c)
-    | GLambda (Name id, k, t, b) ->
+      GLetIn (Anonymous, r, new_b, new_t, new_c)
+    | GLambda (Name id, r, k, t, b) ->
       let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
       let t, b =
         if Id.equal new_id id then (t, b)
@@ -218,8 +219,8 @@ let rec alpha_rt excluded rt =
       let new_excluded = new_id :: excluded in
       let new_t = alpha_rt new_excluded t in
       let new_b = alpha_rt new_excluded b in
-      GLambda (Name new_id, k, new_t, new_b)
-    | GProd (Name id, k, t, b) ->
+      GLambda (Name new_id, r, k, new_t, new_b)
+    | GProd (Name id, r, k, t, b) ->
       let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
       let new_excluded = new_id :: excluded in
       let t, b =
@@ -230,8 +231,8 @@ let rec alpha_rt excluded rt =
       in
       let new_t = alpha_rt new_excluded t in
       let new_b = alpha_rt new_excluded b in
-      GProd (Name new_id, k, new_t, new_b)
-    | GLetIn (Name id, b, t, c) ->
+      GProd (Name new_id, r, k, new_t, new_b)
+    | GLetIn (Name id, r, b, t, c) ->
       let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
       let c =
         if Id.equal new_id id then c
@@ -241,7 +242,7 @@ let rec alpha_rt excluded rt =
       let new_b = alpha_rt new_excluded b in
       let new_t = Option.map (alpha_rt new_excluded) t in
       let new_c = alpha_rt new_excluded c in
-      GLetIn (Name new_id, new_b, new_t, new_c)
+      GLetIn (Name new_id, r, new_b, new_t, new_c)
     | GLetTuple (nal, (na, rto), t, b) ->
       let rev_new_nal, new_excluded, mapping =
         List.fold_left
@@ -316,12 +317,12 @@ let is_free_in id =
       (fun ?loc -> function GRef _ -> false | GVar id' -> Id.compare id' id == 0
         | GEvar _ -> false | GPatVar _ -> false
         | GApp (rt, rtl) | GProj (_, rtl, rt) -> List.exists is_free_in (rt :: rtl)
-        | GLambda (n, _, t, b) | GProd (n, _, t, b) ->
+        | GLambda (n, _, _, t, b) | GProd (n, _, _, t, b) ->
           let check_in_b =
             match n with Name id' -> not (Id.equal id' id) | _ -> true
           in
           is_free_in t || (check_in_b && is_free_in b)
-        | GLetIn (n, b, t, c) ->
+        | GLetIn (n, _, b, t, c) ->
           let check_in_c =
             match n with Name id' -> not (Id.equal id' id) | _ -> true
           in
@@ -383,16 +384,17 @@ let replace_var_by_term x_id term =
           GApp (replace_var_by_pattern rt', List.map replace_var_by_pattern rtl)
         | GProj (f, rtl, rt) ->
           GProj (f, List.map replace_var_by_pattern rtl, replace_var_by_pattern rt)
-        | GLambda (Name id, _, _, _) as rt when Id.compare id x_id == 0 -> rt
-        | GLambda (name, k, t, b) ->
-          GLambda (name, k, replace_var_by_pattern t, replace_var_by_pattern b)
-        | GProd (Name id, _, _, _) as rt when Id.compare id x_id == 0 -> rt
-        | GProd (name, k, t, b) ->
-          GProd (name, k, replace_var_by_pattern t, replace_var_by_pattern b)
-        | GLetIn (Name id, _, _, _) as rt when Id.compare id x_id == 0 -> rt
-        | GLetIn (name, def, typ, b) ->
+        | GLambda (Name id, _, _, _, _) as rt when Id.compare id x_id == 0 -> rt
+        | GLambda (name, r, k, t, b) ->
+          GLambda (name, r, k, replace_var_by_pattern t, replace_var_by_pattern b)
+        | GProd (Name id, _, _, _, _) as rt when Id.compare id x_id == 0 -> rt
+        | GProd (name, r, k, t, b) ->
+          GProd (name, r, k, replace_var_by_pattern t, replace_var_by_pattern b)
+        | GLetIn (Name id, _, _, _, _) as rt when Id.compare id x_id == 0 -> rt
+        | GLetIn (name, r, def, typ, b) ->
           GLetIn
             ( name
+            , r
             , replace_var_by_pattern def
             , Option.map replace_var_by_pattern typ
             , replace_var_by_pattern b )
@@ -510,12 +512,12 @@ let expand_as =
         try DAst.get (Id.Map.find id map) with Not_found -> rt )
       | GApp (f, args) -> GApp (expand_as map f, List.map (expand_as map) args)
       | GProj (f, args, c) -> GProj (f, List.map (expand_as map) args, expand_as map c)
-      | GLambda (na, k, t, b) ->
-        GLambda (na, k, expand_as map t, expand_as map b)
-      | GProd (na, k, t, b) -> GProd (na, k, expand_as map t, expand_as map b)
-      | GLetIn (na, v, typ, b) ->
+      | GLambda (na, r, k, t, b) ->
+        GLambda (na, r, k, expand_as map t, expand_as map b)
+      | GProd (na, r, k, t, b) -> GProd (na, r, k, expand_as map t, expand_as map b)
+      | GLetIn (na, r, v, typ, b) ->
         GLetIn
-          (na, expand_as map v, Option.map (expand_as map) typ, expand_as map b)
+          (na, r, expand_as map v, Option.map (expand_as map) typ, expand_as map b)
       | GLetTuple (nal, (na, po), v, b) ->
         GLetTuple
           ( nal
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5707dab96435f..d3a6b68ff8b5f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -41,9 +41,9 @@ let chop_rlambda_n =
     if n == 0 then (List.rev acc, rt)
     else
       match DAst.get rt with
-      | Glob_term.GLambda (name, k, t, b) ->
+      | Glob_term.GLambda (name, _, k, t, b) ->
         chop_lambda_n ((name, t, None) :: acc) (n - 1) b
-      | Glob_term.GLetIn (name, v, t, b) ->
+      | Glob_term.GLetIn (name, _, v, t, b) ->
         chop_lambda_n ((name, v, t) :: acc) (n - 1) b
       | _ ->
         CErrors.user_err
@@ -56,7 +56,7 @@ let chop_rprod_n =
     if n == 0 then (List.rev acc, rt)
     else
       match DAst.get rt with
-      | Glob_term.GProd (name, k, t, b) ->
+      | Glob_term.GProd (name, _, k, t, b) ->
         chop_prod_n ((name, t) :: acc) (n - 1) b
       | _ ->
         CErrors.user_err
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index a6edd7a6eadde..f8bdc11d9f03f 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -72,7 +72,7 @@ GRAMMAR EXTEND Gram
   Constr.closed_binder: TOP
     [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> {
           let typ = mkAppC (sigref loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-          [CLocalAssum ([id], default_binder_kind, typ)] }
+          [CLocalAssum ([id], None, default_binder_kind, typ)] }
     ] ];
 
   END
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 1bd3bd5213311..450dd2b8e7044 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -111,7 +111,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
           (try List.index Names.Name.equal x.CAst.v ids
           with Not_found -> user_err ~loc Pp.(str "No such fix variable."))
       | _ -> user_err ~loc Pp.(str "Cannot guess decreasing argument of fix.") in
-  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
+  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,None,bk,t)) bl in
   (id,n, CAst.make ~loc @@ CProdN(bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
@@ -120,7 +120,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
         (Pp.str"Annotation forbidden in cofix expression."))
       ann
   in
-  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
+  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,None,bk,t)) bl in
   (id,if bl = [] then ty else CAst.make ~loc @@ CProdN(bl,ty))
 
 (* Functions overloaded by quotifier *)
@@ -156,7 +156,7 @@ let mkTacCase with_evar = function
 let rec mkCLambdaN_simple_loc ?loc bll c =
   match bll with
   | ({CAst.loc = loc1}::_ as idl,bk,t) :: bll ->
-      CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
+      CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,None,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
   | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c
   | [] -> c
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d586bf69083a8..f59680910f117 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -361,7 +361,7 @@ let string_of_genarg_arg (ArgumentType arg) =
       match ty.CAst.v with
           Constrexpr.CProdN(bll,a) ->
             let bll = List.map (function
-            | CLocalAssum (nal,_,t) -> nal,t
+            | CLocalAssum (nal,_,_,t) -> nal,t
             | _ -> user_err Pp.(str "Cannot translate fix tactic: not only products")) bll in
             let nb = List.fold_left (fun i (nal,t) -> i + List.length nal) 0 bll in
             if nb >= n then (List.rev (bll@acc)), a
@@ -1080,7 +1080,7 @@ let pr_goal_selector ~toplevel s =
     let rec strip_ty acc n ty =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
         match DAst.get ty with
-            Glob_term.GProd(na,Glob_term.Explicit,a,b) ->
+            Glob_term.GProd(na,_,Glob_term.Explicit,a,b) ->
               strip_ty (([CAst.make na],(a,None))::acc) (n-1) b
           | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5e73a3faf01fe..dc7cbd9021d96 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -124,10 +124,10 @@ let mkRltacVar id = DAst.make @@ GVar (id)
 let mkRCast rc rt =  DAst.make @@ GCast (rc, Some DEFAULTcast, rt)
 let mkRType =  DAst.make @@ GSort (UAnonymous {rigid=UnivRigid})
 let mkRProp =  DAst.make @@ GSort (UNamed (None, [GProp, 0]))
-let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
+let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, None, Explicit, rt1, rt2)
 let mkRConstruct c = DAst.make @@ GRef (GlobRef.ConstructRef c,None)
 let mkRInd mind = DAst.make @@ GRef (GlobRef.IndRef mind,None)
-let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
+let mkRLambda n s t = DAst.make @@ GLambda (n, None, Explicit, s, t)
 
 let rec mkRnat n =
   if n <= 0 then DAst.make @@ GRef (Coqlib.lib_ref "num.nat.O", None) else
@@ -717,9 +717,9 @@ let rec mkCHoles ?loc n =
   if n <= 0 then [] else (CAst.make ?loc @@ CHole (None)) :: mkCHoles ?loc (n - 1)
 let mkCHole loc = CAst.make ?loc @@ CHole (None)
 let mkCLambda ?loc name ty t =  CAst.make ?loc @@
-   CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
+   CLambdaN ([CLocalAssum([CAst.make ?loc name], None, Default Explicit, ty)], t)
 let mkCArrow ?loc ty t = CAst.make ?loc @@
-   CProdN ([CLocalAssum([CAst.make Anonymous], Default Explicit, ty)], t)
+   CProdN ([CLocalAssum([CAst.make Anonymous], None, Default Explicit, ty)], t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, Some DEFAULTcast, ty)
 
 let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = []
@@ -730,14 +730,14 @@ let pf_interp_ty ?(resolve_typeclasses=false) env sigma0 ist ty =
    let ty = match ty with
    | a, (t, None) ->
     let rec force_type ty = DAst.(map (function
-     | GProd (x, k, s, t) -> incr n_binders; GProd (x, k, s, force_type t)
-     | GLetIn (x, v, oty, t) -> incr n_binders; GLetIn (x, v, oty, force_type t)
+     | GProd (x, r, k, s, t) -> incr n_binders; GProd (x, r, k, s, force_type t)
+     | GLetIn (x, r, v, oty, t) -> incr n_binders; GLetIn (x, r, v, oty, force_type t)
      | _ -> DAst.get (mkRCast ty mkRType))) ty in
      a, (force_type t, None)
    | _, (_, Some ty) ->
     let rec force_type ty = CAst.(map (function
      | CProdN (abs, t) ->
-       n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern _ -> (* We count a 'pat for 1; TO BE CHECKED *) [CAst.make Name.Anonymous]) abs));
+       n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_,_) -> nal | CLocalDef (na,_,_,_) -> [na] | CLocalPattern _ -> (* We count a 'pat for 1; TO BE CHECKED *) [CAst.make Name.Anonymous]) abs));
        CProdN (abs, force_type t)
      | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t)
      | _ -> (mkCCast ty (mkCType None)).v)) ty in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7515f9a388466..8718e728ed05c 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1213,19 +1213,19 @@ let pr_binder prl = function
     str ": " ++ prl t
 
 let rec format_local_binders h0 bl0 = match h0, bl0 with
-  | BFvar :: h, CLocalAssum ([{CAst.v=x}], _,  _) :: bl ->
+  | BFvar :: h, CLocalAssum ([{CAst.v=x}], _, _,  _) :: bl ->
     Bvar x :: format_local_binders h bl
-  | BFdecl _ :: h, CLocalAssum (lxs, _, t) :: bl ->
+  | BFdecl _ :: h, CLocalAssum (lxs, _, _, t) :: bl ->
     Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: format_local_binders h bl
-  | BFdef :: h, CLocalDef ({CAst.v=x}, v, oty) :: bl ->
+  | BFdef :: h, CLocalDef ({CAst.v=x}, _, v, oty) :: bl ->
     Bdef (x, oty, v) :: format_local_binders h bl
   | _ -> []
 
 let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
-  | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _)], c) } ->
+  | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _, _)], c) } ->
     let bs, c' = format_constr_expr h c in
     Bvar x :: bs, c'
-  | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } ->
+  | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, _, t)], c) } ->
     let bs, c' = format_constr_expr h c in
     Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: bs, c'
   | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
@@ -1234,11 +1234,11 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
   | [BFcast], { v = CCast (c, defaultCast, t) } ->
     [Bcast t], c
   | BFrec (has_str, has_cast) :: h,
-    { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } ->
+    { v = CFix ( _, [_, _, Some {CAst.v = CStructRec locn}, bl, t, c]) } ->
     let bs = format_local_binders h bl in
     let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in
     bs @ bstr @ (if has_cast then [Bcast t] else []), c
-  | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } ->
+  | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, _, bl, t, c]) } ->
     format_local_binders h bl @ (if has_cast then [Bcast t] else []), c
   | _, c ->
     [], c
@@ -1340,20 +1340,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde
  | [ ssrbvar(bv) ] ->
    { let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],None,Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
  | [ "(" ssrbvar(bv) ")" ] ->
    { let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],None,Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
  | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
    { let x = bvar_lname bv in
      (FwdPose, [BFdecl 1]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], None, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
  | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] ->
    { let xs = List.map bvar_lname (bv :: bvs) in
      let n = List.length xs in
      (FwdPose, [BFdecl n]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, None, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
  | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
    { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) }
  | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
@@ -1365,7 +1365,7 @@ GRAMMAR EXTEND Gram
   ssrbinder: TOP [
   [  ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> {
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],None,Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
   ];
 END
 
@@ -1393,10 +1393,10 @@ let push_binders c2 bs =
   | ct -> loop false ct bs
 
 let rec fix_binders = let open CAst in function
-  | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs ->
-      CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs
+  | (_, { v = CLambdaN ([CLocalAssum(xs, _, _, t)], _) } ) :: bs ->
+      CLocalAssum (xs, None, Default Glob_term.Explicit, t) :: fix_binders bs
   | (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
-    CLocalDef (x, v, oty) :: fix_binders bs
+    CLocalDef (x, None, v, oty) :: fix_binders bs
   | _ -> []
 
 let pr_ssrstruct _ _ _ = function
@@ -1457,7 +1457,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS (ident * ssrfwd) PRINTED BY { pr_ssrfixfwd }
           | [] -> CErrors.user_err (Pp.str "Bad structural argument") in
         loop (names_of_local_assums lb) in
       let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in
-      let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some (CAst.make (CStructRec i))), lb, t', c']) in
+      let fix = CAst.make ~loc @@ CFix (lid, [lid, None, (Some (CAst.make (CStructRec i))), lb, t', c']) in
       id, ((fk, h'),  { ac with body = fix }) }
 END
 
@@ -1479,7 +1479,7 @@ ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY { pr_ssrcofixfwd }
       | [Bcast t'], c' -> true, t', c'
       | _ -> false, mkCHole (constr_loc c), c in
       let h' = BFrec (false, has_cast) :: binders_fmts bs in
-      let cofix = CAst.make ~loc @@ CCoFix (lid, [lid, fix_binders bs, t', c']) in
+      let cofix = CAst.make ~loc @@ CCoFix (lid, [lid, None, fix_binders bs, t', c']) in
       id, ((fk, h'), { ac with body = cofix })
     }
 END
@@ -1524,13 +1524,13 @@ let intro_id_to_binder = List.map (function
   | IPatId id ->
       let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
       (FwdPose, [BFvar]),
-        CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)],
+        CAst.make @@ CLambdaN ([CLocalAssum([x], None, Default Glob_term.Explicit, mkCHole xloc)],
           mkCHole None)
   | _ -> anomaly "non-id accepted as binder")
 
 let binder_to_intro_id = CAst.(List.map (function
-  | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) }
-  | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } ->
+  | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_,_)],_) }
+  | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_,_)],_) } ->
       List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon (One None)) ids
   | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id]
   | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)]
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index dbd28c0f198cb..de133bd469373 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -121,7 +121,7 @@ GRAMMAR EXTEND Gram
   GLOBAL: closed_binder;
   closed_binder: TOP [
     [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" ->
-      { [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] }
+      { [CLocalAssum ([CAst.make ~loc Anonymous], None, Default Explicit, c)] }
   ] ];
 END
 
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 294906da1505f..cd8f2825eca74 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -123,13 +123,13 @@ let destCVar = function
     qualid_basename qid
   | _ ->
     CErrors.anomaly (str"not a CRef.")
-let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false
-let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
+let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _, _) -> true | _ -> false
+let destGLambda c = match DAst.get c with GLambda (Name id, _, _, _, c) -> (id, c)
   | _ -> CErrors.anomaly (str "not a GLambda")
 let isGHole c = match DAst.get c with GHole _ -> true | _ -> false
 let mkCHole ~loc = CAst.make ?loc @@ CHole (None)
 let mkCLambda ?loc name ty t = CAst.make ?loc @@
-   CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
+   CLambdaN ([CLocalAssum([CAst.make ?loc name], None, Default Explicit, ty)], t)
 let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((CAst.make ?loc name), bo, None, t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, Some DEFAULTcast, ty)
@@ -138,7 +138,7 @@ let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, Some DEFAULTcast, ty)
 let mkRHole = DAst.make @@ GHole (GInternalHole)
 let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
 let mkRCast rc rt =  DAst.make @@ GCast (rc, Some DEFAULTcast, rt)
-let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
+let mkRLambda n s t = DAst.make @@ GLambda (n, None, Explicit, s, t)
 
 (* }}} *)
 
@@ -1154,7 +1154,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
   | Some b -> {kind; pattern=(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)); interpretation}
   | None -> { kind
             ; pattern = DAst.make ?loc @@ GLetIn
-                  (x, DAst.make ?loc @@ GHole (GBinderType x), None, g), None
+                  (x, None, DAst.make ?loc @@ GHole (GBinderType x), None, g), None
             ; interpretation} in
   match red with
   | T t -> let sigma, t = interp_term env sigma0 t in { pat_sigma = sigma; pat_pat = T t }
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index eb2fc6f377dcf..a46f7236bc614 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -341,6 +341,58 @@ let { Goptions.get = print_match_paramunivs } =
     ~value:false
     ()
 
+let { Goptions.get = print_relevances } =
+  Goptions.declare_bool_option_and_ref
+    ~key:["Printing";"Relevance";"Marks"]
+    ~value:false
+    ()
+
+(** univ and sort detyping *)
+
+let detype_level_name sigma l =
+  if Univ.Level.is_set l then GSet else
+    match UState.id_of_level (Evd.evar_universe_context sigma) l with
+    | Some id -> GLocalUniv (CAst.make id)
+    | None -> GUniv l
+
+let detype_level sigma l =
+  UNamed (detype_level_name sigma l)
+
+let detype_qvar sigma q =
+  match UState.id_of_qvar (Evd.evar_universe_context sigma) q with
+  | Some id -> GLocalQVar (CAst.make (Name id))
+  | None -> GQVar q
+
+let detype_quality sigma q =
+  let open Sorts.Quality in
+  match q with
+  | QConstant q -> GQConstant q
+  | QVar q -> GQualVar (detype_qvar sigma q)
+
+let detype_universe sigma u =
+  List.map (on_fst (detype_level_name sigma)) (Univ.Universe.repr u)
+
+let detype_sort sigma = function
+  | SProp -> UNamed (None, [GSProp,0])
+  | Prop -> UNamed (None, [GProp,0])
+  | Set -> UNamed (None, [GSet,0])
+  | Type u ->
+      (if !print_universes
+       then UNamed (None, detype_universe sigma u)
+       else UAnonymous {rigid=UnivRigid})
+  | QSort (q, u) ->
+    if !print_universes then
+      let q = if print_sort_quality () then Some (detype_qvar sigma q) else None in
+      UNamed (q, detype_universe sigma u)
+    else UAnonymous {rigid=UnivRigid}
+
+let detype_relevance_info sigma na =
+  if not (print_relevances ()) then None
+  else match Evarutil.nf_relevance sigma na.binder_relevance with
+    | Relevant -> Some GRelevant
+    | Irrelevant -> Some GIrrelevant
+    | RelevanceVar q -> Some (GRelevanceVar (detype_qvar sigma q))
+
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
 
@@ -554,8 +606,8 @@ let extract_nondep_branches b l =
   let rec strip l r =
     match DAst.get r, l with
       | r', [] -> r
-      | GLambda (_,_,_,t), false::l -> strip l t
-      | GLetIn (_,_,_,t), true::l -> strip l t
+      | GLambda (_,_,_,_,t), false::l -> strip l t
+      | GLetIn (_,_,_,_,t), true::l -> strip l t
       (* FIXME: do we need adjustment? *)
       | _,_ -> assert false in
   strip l b
@@ -564,8 +616,8 @@ let it_destRLambda_or_LetIn_names l c =
   let rec aux l nal c =
     match DAst.get c, l with
       | _, [] -> (List.rev nal,c)
-      | GLambda (na,_,_,c), false::l -> aux l (na::nal) c
-      | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c
+      | GLambda (na,_,_,_,c), false::l -> aux l (na::nal) c
+      | GLetIn (na,_,_,_,c), true::l -> aux l (na::nal) c
       | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c
       | _, false::l ->
           (* eta-expansion *)
@@ -612,7 +664,7 @@ let detype_case computable detype detype_eqns avoid env sigma (ci, univs, params
       let p = detype p in
       let nl,typ = it_destRLambda_or_LetIn_names ci.ci_pp_info.ind_tags p in
       let n,typ = match DAst.get typ with
-        | GLambda (x,_,t,c) -> x, c
+        | GLambda (x,_,_,t,c) -> x, c
         | _ -> Anonymous, typ in
       let aliastyp =
         if List.for_all (Name.equal Anonymous) nl then None
@@ -671,7 +723,7 @@ let rec share_names detype flags n l avoid env sigma c t =
         let t' = detype flags avoid env sigma t in
         let id, avoid = next_name_away flags na.binder_name avoid in
         let env = add_name (set_name (Name id) decl) env in
-        share_names detype flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+        share_names detype flags (n-1) ((Name id,detype_relevance_info sigma na, Explicit,None,t')::l) avoid env sigma c c'
     (* May occur for fix built interactively *)
     | LetIn (na,b,t',c), _ when n > 0 ->
         let decl = LocalDef (na,b,t') in
@@ -679,7 +731,7 @@ let rec share_names detype flags n l avoid env sigma c t =
         let b' = detype flags avoid env sigma b in
         let id, avoid = next_name_away flags na.binder_name avoid in
         let env = add_name (set_name (Name id) decl) env in
-        share_names detype flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
+        share_names detype flags n ((Name id,detype_relevance_info sigma na, Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
     (* Only if built with the f/n notation or w/o let-expansion in types *)
     | _, LetIn (_,b,_,t) when n > 0 ->
         share_names detype flags n l avoid env sigma c (subst1 b t)
@@ -690,7 +742,7 @@ let rec share_names detype flags n l avoid env sigma c t =
         let id, avoid = next_name_away flags na'.binder_name avoid in
         let env = add_name (set_name (Name id) decl) env in
         let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-        share_names detype flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
+        share_names detype flags (n-1) ((Name id,detype_relevance_info sigma na',Explicit,None,t'')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
         if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
@@ -714,7 +766,7 @@ let rec share_pattern_names detype n l avoid env sigma c t =
         let id = Namegen.next_name_away na avoid in
         let avoid = Id.Set.add id avoid in
         let env = Name id :: env in
-        share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+        share_pattern_names detype (n-1) ((Name id,None,Explicit,None,t')::l) avoid env sigma c c'
     | _ ->
         if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
         let c = detype avoid env sigma c in
@@ -753,43 +805,6 @@ let detype_cofix detype flags avoid env sigma n (names,tys,bodies) =
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-let detype_level_name sigma l =
-  if Univ.Level.is_set l then GSet else
-    match UState.id_of_level (Evd.evar_universe_context sigma) l with
-    | Some id -> GLocalUniv (CAst.make id)
-    | None -> GUniv l
-
-let detype_level sigma l =
-  UNamed (detype_level_name sigma l)
-
-let detype_qvar sigma q =
-  match UState.id_of_qvar (Evd.evar_universe_context sigma) q with
-  | Some id -> GLocalQVar (CAst.make (Name id))
-  | None -> GQVar q
-
-let detype_quality sigma q =
-  let open Sorts.Quality in
-  match q with
-  | QConstant q -> GQConstant q
-  | QVar q -> GQualVar (detype_qvar sigma q)
-
-let detype_universe sigma u =
-  List.map (on_fst (detype_level_name sigma)) (Univ.Universe.repr u)
-
-let detype_sort sigma = function
-  | SProp -> UNamed (None, [GSProp,0])
-  | Prop -> UNamed (None, [GProp,0])
-  | Set -> UNamed (None, [GSet,0])
-  | Type u ->
-      (if !print_universes
-       then UNamed (None, detype_universe sigma u)
-       else UAnonymous {rigid=UnivRigid})
-  | QSort (q, u) ->
-    if !print_universes then
-      let q = if print_sort_quality () then Some (detype_qvar sigma q) else None in
-      UNamed (q, detype_universe sigma u)
-    else UAnonymous {rigid=UnivRigid}
-
 type binder_kind = BProd | BLambda | BLetIn
 
 (**********************************************************************)
@@ -1014,13 +1029,14 @@ and detype_binder d flags bk avoid env sigma decl c =
   let na = get_name decl in
   let body = get_value decl in
   let ty = get_type decl in
+  let rinfo = detype_relevance_info sigma (get_annot decl) in
   let na',avoid' = match bk with
   | BLetIn -> compute_name sigma ~let_in:true ~pattern:false flags avoid env na c
   | _ -> compute_name sigma ~let_in:false ~pattern:false flags avoid env na c in
   let r =  detype d flags avoid' (add_name (set_name na' decl) env) sigma c in
   match bk with
-  | BProd   -> GProd (na',Explicit,detype d (nongoal flags) avoid env sigma ty, r)
-  | BLambda -> GLambda (na',Explicit,detype d (nongoal flags) avoid env sigma ty, r)
+  | BProd   -> GProd (na',rinfo,Explicit,detype d (nongoal flags) avoid env sigma ty, r)
+  | BLambda -> GLambda (na',rinfo,Explicit,detype d (nongoal flags) avoid env sigma ty, r)
   | BLetIn ->
       let c = detype d { flg_isgoal = false } avoid env sigma (Option.get body) in
       (* Heuristic: we display the type if in Prop *)
@@ -1033,7 +1049,7 @@ and detype_binder d flags bk avoid env sigma decl c =
           with Retyping.RetypeError _ -> InType
       in
       let t = if s != InProp  && not !Flags.raw_print then None else Some (detype d (nongoal flags) avoid env sigma ty) in
-      GLetIn (na', c, t, r)
+      GLetIn (na', rinfo, c, t, r)
 
 let detype_rel_context d flags where avoid env sigma sign =
   let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
@@ -1042,6 +1058,7 @@ let detype_rel_context d flags where avoid env sigma sign =
   | decl::rest ->
       let na = get_name decl in
       let t = get_type decl in
+      let r = detype_relevance_info sigma (get_annot decl) in
       let na',avoid' =
         match where with
         | None -> na,avoid
@@ -1054,7 +1071,7 @@ let detype_rel_context d flags where avoid env sigma sign =
       in
       let b' = Option.map (detype d flags avoid env sigma) b in
       let t' = detype d flags avoid env sigma t in
-      (na',Explicit,b',t') :: aux avoid' (add_name (set_name na' decl) env) rest
+      (na',r,Explicit,b',t') :: aux avoid' (add_name (set_name na' decl) env) rest
   in aux avoid env (List.rev sign)
 
 let detype d ?(isgoal=false) avoid env sigma t =
@@ -1099,15 +1116,15 @@ let detype_closed_glob ?isgoal avoid env sigma t =
         with Not_found ->
          GVar id
         end
-    | GLambda (id,k,t,c) ->
+    | GLambda (id,r,k,t,c) ->
         let id = convert_name cl id in
-        GLambda(id,k,detype_closed_glob cl t, detype_closed_glob cl c)
-    | GProd (id,k,t,c) ->
+        GLambda(id,r,k,detype_closed_glob cl t, detype_closed_glob cl c)
+    | GProd (id,r,k,t,c) ->
         let id = convert_name cl id in
-        GProd(id,k,detype_closed_glob cl t, detype_closed_glob cl c)
-    | GLetIn (id,b,t,e) ->
+        GProd(id,r,k,detype_closed_glob cl t, detype_closed_glob cl c)
+    | GLetIn (id,r,b,t,e) ->
         let id = convert_name cl id in
-        GLetIn(id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e)
+        GLetIn(id,r,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e)
     | GLetTuple (ids,(n,r),b,e) ->
         let ids = List.map (convert_name cl) ids in
         let n = convert_name cl n in
@@ -1170,22 +1187,22 @@ let rec subst_glob_constr env subst = DAst.map (function
         if ref' == ref && rl' == rl && r' == r then raw else
           GProj((destConstRef ref',u),rl',r')
 
-  | GLambda (n,bk,r1,r2) as raw ->
+  | GLambda (n,r,bk,r1,r2) as raw ->
       let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in
         if r1' == r1 && r2' == r2 then raw else
-          GLambda (n,bk,r1',r2')
+          GLambda (n,r,bk,r1',r2')
 
-  | GProd (n,bk,r1,r2) as raw ->
+  | GProd (n,r,bk,r1,r2) as raw ->
       let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in
         if r1' == r1 && r2' == r2 then raw else
-          GProd (n,bk,r1',r2')
+          GProd (n,r,bk,r1',r2')
 
-  | GLetIn (n,r1,t,r2) as raw ->
+  | GLetIn (n,r,r1,t,r2) as raw ->
       let r1' = subst_glob_constr env subst r1 in
       let r2' = subst_glob_constr env subst r2 in
       let t' = Option.Smart.map (subst_glob_constr env subst) t in
         if r1' == r1 && t == t' && r2' == r2 then raw else
-          GLetIn (n,r1',t',r2')
+          GLetIn (n,r,r1',t',r2')
 
   | GCases (sty,rtno,rl,branches) as raw ->
     let open CAst in
@@ -1229,10 +1246,10 @@ let rec subst_glob_constr env subst = DAst.map (function
       let ra1' = Array.Smart.map (subst_glob_constr env subst) ra1
       and ra2' = Array.Smart.map (subst_glob_constr env subst) ra2 in
       let bl' = Array.Smart.map
-        (List.Smart.map (fun (na,k,obd,ty as dcl) ->
+        (List.Smart.map (fun (na,r,k,obd,ty as dcl) ->
           let ty' = subst_glob_constr env subst ty in
           let obd' = Option.Smart.map (subst_glob_constr env subst) obd in
-          if ty'==ty && obd'==obd then dcl else (na,k,obd',ty')))
+          if ty'==ty && obd'==obd then dcl else (na,r,k,obd',ty')))
         bl in
         if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
           GRec (fix,ida,bl',ra1',ra2')
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index b81de87535a23..89e5c4dd80c74 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -56,10 +56,10 @@ val detype_rel_context : 'a delay -> constr option -> Id.Set.t -> (names_context
 
 val share_pattern_names :
   (Id.Set.t -> names_context -> 'c -> 'd Pattern.constr_pattern_r -> 'a) -> int ->
-  (Name.t * binding_kind * 'b option * 'a) list ->
+  (Name.t * 'e option * binding_kind * 'b option * 'a) list ->
   Id.Set.t -> names_context -> 'c -> 'd Pattern.constr_pattern_r ->
   'd Pattern.constr_pattern_r ->
-  (Name.t * binding_kind * 'b option * 'a) list * 'a * 'a
+  (Name.t * 'e option * binding_kind * 'b option * 'a) list * 'a * 'a
 
 val detype_closed_glob :  ?isgoal:bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 742713d0c80d3..7b555b468f261 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -39,10 +39,10 @@ let mkGApp ?loc p l = DAst.make ?loc @@
   | GApp (f,l') -> GApp (f,l'@l)
   | _          -> GApp (p,l)
 
-let map_glob_decl_left_to_right f (na,k,obd,ty) =
+let map_glob_decl_left_to_right f (na,r,k,obd,ty) =
   let comp1 = Option.map f obd in
   let comp2 = f ty in
-  (na,k,comp1,comp2)
+  (na,r,k,comp1,comp2)
 
 let glob_qvar_eq g1 g2 = match g1, g2 with
   | GLocalQVar na1, GLocalQVar na2 -> CAst.eq Name.equal na1 na2
@@ -103,6 +103,13 @@ let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | MaxImplicit, MaxImplicit -> true
   | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false
 
+let glob_relevance_eq a b = match a, b with
+  | GRelevant, GRelevant | GIrrelevant, GIrrelevant -> true
+  | GRelevanceVar q1, GRelevanceVar q2 -> glob_qvar_eq q1 q2
+  | (GRelevant | GIrrelevant | GRelevanceVar _), _ -> false
+
+let relevance_info_eq = Option.equal glob_relevance_eq
+
 let case_style_eq s1 s2 = let open Constr in match s1, s2 with
   | LetStyle, LetStyle -> true
   | IfStyle, IfStyle -> true
@@ -140,8 +147,8 @@ and cases_clause_eq f g {CAst.v=(id1, p1, c1)} {CAst.v=(id2, p2, c2)} =
   (* In principle, id1 and id2 canonically derive from p1 and p2 *)
   List.equal (mk_cases_pattern_eq g) p1 p2 && f c1 c2
 
-let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) =
-  Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
+let glob_decl_eq f (na1, r1, bk1, c1, t1) (na2, r2, bk2, c2, t2) =
+  Name.equal na1 na2 && relevance_info_eq r1 r2 && binding_kind_eq bk1 bk2 &&
   Option.equal f c1 c2 && f t1 t2
 
 let fix_kind_eq k1 k2 = match k1, k2 with
@@ -163,12 +170,15 @@ let mk_glob_constr_eq f g c1 c2 = match DAst.get c1, DAst.get c2 with
   | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2
   | GApp (f1, arg1), GApp (f2, arg2) ->
     f f1 f2 && List.equal f arg1 arg2
-  | GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) ->
-    g na1 na2 (Some t1) (Some t2) && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2
-  | GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) ->
-    g na1 na2 (Some t1) (Some t2) && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2
-  | GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) ->
-    g na1 na2 t1 t2 && f b1 b2 && Option.equal f t1 t2 && f c1 c2
+  | GLambda (na1, r1, bk1, t1, c1), GLambda (na2, r2, bk2, t2, c2) ->
+    g na1 na2 (Some t1) (Some t2) && relevance_info_eq r1 r2
+    && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2
+  | GProd (na1, r1, bk1, t1, c1), GProd (na2, r2, bk2, t2, c2) ->
+    g na1 na2 (Some t1) (Some t2) && relevance_info_eq r1 r2
+    && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2
+  | GLetIn (na1, r1, b1, t1, c1), GLetIn (na2, r2, b2, t2, c2) ->
+    g na1 na2 t1 t2 && relevance_info_eq r1 r2
+    && f b1 b2 && Option.equal f t1 t2 && f c1 c2
   | GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) ->
     case_style_eq st1 st2 && Option.equal f c1 c2 &&
     List.equal (tomatch_tuple_eq f) tp1 tp2 &&
@@ -226,19 +236,19 @@ let map_glob_constr_left_to_right_with_names f g = DAst.map (function
       let comp1 = f g in
       let comp2 = Util.List.map_left f args in
       GApp (comp1,comp2)
-  | GLambda (na,bk,ty,c) ->
+  | GLambda (na,r,bk,ty,c) ->
       let comp1 = f ty in
       let comp2 = f c in
-      GLambda (g na,bk,comp1,comp2)
-  | GProd (na,bk,ty,c) ->
+      GLambda (g na,r,bk,comp1,comp2)
+  | GProd (na,r,bk,ty,c) ->
       let comp1 = f ty in
       let comp2 = f c in
-      GProd (g na,bk,comp1,comp2)
-  | GLetIn (na,b,t,c) ->
+      GProd (g na,r,bk,comp1,comp2)
+  | GLetIn (na,r,b,t,c) ->
       let comp1 = f b in
       let compt = Option.map f t in
       let comp2 = f c in
-      GLetIn (g na,comp1,compt,comp2)
+      GLetIn (g na,r,comp1,compt,comp2)
   | GCases (sty,rtntypopt,tml,pl) ->
       let comp1 = Option.map f rtntypopt in
       let comp2 = Util.List.map_left (fun (tm,(x,indxl)) -> (f tm,(g x,Option.map (CAst.map (fun (ind,xl) -> (ind,List.map g xl))) indxl))) tml in
@@ -285,9 +295,9 @@ let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt
 let fold_glob_constr f acc = DAst.with_val (function
   | GVar _ -> acc
   | GApp (c,args) -> List.fold_left f (f acc c) args
-  | GLambda (_,_,b,c) | GProd (_,_,b,c) ->
+  | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) ->
     f (f acc b) c
-  | GLetIn (_,b,t,c) ->
+  | GLetIn (_,_,b,t,c) ->
     f (Option.fold_left f (f acc b) t) c
   | GCases (_,rtntypopt,tml,pl) ->
     let fold_pattern acc {CAst.v=(idl,p,c)} = f acc c in
@@ -300,7 +310,7 @@ let fold_glob_constr f acc = DAst.with_val (function
     f (f (f (fold_return_type f acc rtntyp) c) b1) b2
   | GRec (_,_,bl,tyl,bv) ->
     let acc = Array.fold_left
-      (List.fold_left (fun acc (na,k,bbd,bty) ->
+      (List.fold_left (fun acc (_,_,_,bbd,bty) ->
         f (Option.fold_left f acc bbd) bty)) acc bl in
     Array.fold_left f (Array.fold_left f acc tyl) bv
   | GCast (c,k,t) ->
@@ -318,9 +328,9 @@ let fold_return_type_with_binders f g v acc (na,tyopt) =
 let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
   | GVar _ -> acc
   | GApp (c,args) -> List.fold_left (f v) (f v acc c) args
-  | GLambda (na,_,b,c) | GProd (na,_,b,c) ->
+  | GLambda (na,_,_,b,c) | GProd (na,_,_,b,c) ->
     f (Name.fold_right g na v) (f v acc b) c
-  | GLetIn (na,b,t,c) ->
+  | GLetIn (na,_,b,t,c) ->
     f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c
   | GCases (_,rtntypopt,tml,pl) ->
     let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in
@@ -342,7 +352,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
     let f' i acc fid =
       let v,acc =
         List.fold_left
-          (fun (v,acc) (na,k,bbd,bty) ->
+          (fun (v,acc) (na,_,_,bbd,bty) ->
             (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty))
           (v,acc)
           bll.(i) in
@@ -492,15 +502,15 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
   | GRef (GlobRef.VarRef id,_) as r ->
       if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
       else r
-  | GProd (na,bk,t,c) ->
+  | GProd (na,r,bk,t,c) ->
       let na',l' = update_subst na l in
-      GProd (na',bk,rename_glob_vars l t,rename_glob_vars l' c)
-  | GLambda (na,bk,t,c) ->
+      GProd (na',r,bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLambda (na,r,bk,t,c) ->
       let na',l' = update_subst na l in
-      GLambda (na',bk,rename_glob_vars l t,rename_glob_vars l' c)
-  | GLetIn (na,b,t,c) ->
+      GLambda (na',r,bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLetIn (na,r,b,t,c) ->
       let na',l' = update_subst na l in
-      GLetIn (na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c)
+      GLetIn (na',r,rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c)
   (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
   | GCases (ci,po,tomatchl,cls) ->
       let test_pred_pat (na,ino) =
@@ -521,8 +531,9 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
   | GRec (k,idl,decls,bs,ts) ->
      Array.iter (test_id l) idl;
      GRec (k,idl,
-           Array.map (List.map (fun (na,k,bbd,bty) ->
-             test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls,
+           Array.map (List.map (fun (na,r,k,bbd,bty) ->
+               test_na l na;
+               (na,r,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls,
            Array.map (rename_glob_vars l) bs,
            Array.map (rename_glob_vars l) ts)
   | _ -> DAst.get (map_glob_constr (rename_glob_vars l) c)
@@ -559,7 +570,7 @@ let rec cases_pattern_of_glob_constr env na c =
       PatCstr (cstr,List.map (cases_pattern_of_glob_constr env Anonymous) l,na)
     | _ -> raise Not_found
     end
-  | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous ->
+  | GLetIn (Name id as na',_,b,None,e) when is_gvar id e && na = Anonymous ->
      (* A canonical encoding of aliases *)
      DAst.get (cases_pattern_of_glob_constr env na' b)
   | _ -> raise Not_found
@@ -598,7 +609,7 @@ let add_patterns_for_params_remove_local_defs env (ind,j) l =
 let add_alias ?loc na c =
   match na with
   | Anonymous -> c
-  | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id))
+  | Name id -> GLetIn (na,None,DAst.make ?loc c,None,DAst.make ?loc (GVar id))
 
 (* Turn a closed cases pattern into a glob_constr *)
 let rec glob_constr_of_cases_pattern_aux env isclosed x = DAst.map_with_loc (fun ?loc -> function
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 07d05f9fec8ed..3d4b2389d177e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -25,6 +25,8 @@ val glob_quality_eq :  glob_quality -> glob_quality -> bool
 
 val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
 
+val relevance_info_eq : relevance_info -> relevance_info -> bool
+
 val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
 (** Expect a Prop/SProp/Set/Type universe; raise [ComplexSort] if
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index ec1bd2521ff8c..dfd9330df6b90 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -27,6 +27,10 @@ type glob_qvar =
   | GQVar of Sorts.QVar.t
   | GRawQVar of Sorts.QVar.t (* hack for funind *)
 
+type glob_relevance =
+  | GRelevant | GIrrelevant
+  | GRelevanceVar of glob_qvar
+
 type glob_quality =
   | GQConstant of Sorts.Quality.constant
   | GQualVar of glob_qvar
@@ -76,6 +80,8 @@ type cases_pattern = [ `any ] cases_pattern_g
 
 type binding_kind = Explicit | MaxImplicit | NonMaxImplicit
 
+type relevance_info = glob_relevance option
+
 type glob_evar_kind = Evar_kinds.glob_evar_kind =
   | GImplicitArg of GlobRef.t * (int * Id.t option) * bool (** Force inference *)
   | GBinderType of Name.t
@@ -96,9 +102,9 @@ type 'a glob_constr_r =
   | GEvar   of existential_name CAst.t * (lident * 'a glob_constr_g) list
   | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
   | GApp    of 'a glob_constr_g * 'a glob_constr_g list
-  | GLambda of Name.t * binding_kind *  'a glob_constr_g * 'a glob_constr_g
-  | GProd   of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g
-  | GLetIn  of Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g
+  | GLambda of Name.t * relevance_info * binding_kind *  'a glob_constr_g * 'a glob_constr_g
+  | GProd   of Name.t * relevance_info * binding_kind * 'a glob_constr_g * 'a glob_constr_g
+  | GLetIn  of Name.t * relevance_info * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g
   | GCases  of Constr.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g
       (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
   | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
@@ -115,7 +121,7 @@ type 'a glob_constr_r =
   | GArray of glob_instance option * 'a glob_constr_g array * 'a glob_constr_g * 'a glob_constr_g
 and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
 
-and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
+and 'a glob_decl_g = Name.t * relevance_info * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
 
 and 'a predicate_pattern_g =
     Name.t * (inductive * Name.t list) CAst.t option
@@ -150,8 +156,8 @@ type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g
 type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g
 
 type 'a extended_glob_local_binder_r =
-  | GLocalAssum   of Name.t * binding_kind * 'a glob_constr_g
-  | GLocalDef     of Name.t * 'a glob_constr_g * 'a glob_constr_g option
+  | GLocalAssum   of Name.t * relevance_info * binding_kind * 'a glob_constr_g
+  | GLocalDef     of Name.t * relevance_info * 'a glob_constr_g * 'a glob_constr_g option
   | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g
 and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 2c6edb9eb3457..5e9fb9846b9a1 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -451,15 +451,15 @@ let rec pat_of_raw metas vars : _ -> pkind constr_pattern_r = DAst.with_loc_val
       PProj (p, pat_of_raw metas vars c)
     else
       PApp (PRef (GlobRef.ConstRef p), Array.map_of_list (pat_of_raw metas vars) (cl @ [c]))
-  | GLambda (na,bk,c1,c2) ->
+  | GLambda (na,_,bk,c1,c2) ->
       Name.iter (fun n -> push_meta metas n) na;
       PLambda (na, pat_of_raw metas vars c1,
                pat_of_raw metas (na::vars) c2)
-  | GProd (na,bk,c1,c2) ->
+  | GProd (na,_,bk,c1,c2) ->
       Name.iter (fun n -> push_meta metas n) na;
       PProd (na, pat_of_raw metas vars c1,
                pat_of_raw metas (na::vars) c2)
-  | GLetIn (na,c1,t,c2) ->
+  | GLetIn (na,_,c1,t,c2) ->
       Name.iter (fun n -> push_meta metas n) na;
       PLetIn (na, pat_of_raw metas vars c1,
                Option.map (pat_of_raw metas vars) t,
@@ -564,7 +564,7 @@ let rec pat_of_raw metas vars : _ -> pkind constr_pattern_r = DAst.with_loc_val
 
 and pat_of_glob_in_context metas vars decls c =
   let rec aux acc vars = function
-    | (na,bk,b,t) :: decls ->
+    | (na,_,bk,b,t) :: decls ->
        let decl = (na,bk,Option.map (pat_of_raw metas vars) b,pat_of_raw metas vars t) in
        aux (decl::acc) (na::vars) decls
     | [] ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3e87471a1f8f0..3c269bfa11863 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -594,11 +594,11 @@ let eval_pretyper self ~flags tycon env sigma t =
     self.pretype_app self (c, args) ?loc ~flags tycon env sigma
   | GProj (hd, args, c) ->
     self.pretype_proj self (hd, args, c) ?loc ~flags tycon env sigma
-  | GLambda (na, bk, t, c) ->
+  | GLambda (na, _, bk, t, c) ->
     self.pretype_lambda self (na, bk, t, c) ?loc ~flags tycon env sigma
-  | GProd (na, bk, t, c) ->
+  | GProd (na, _, bk, t, c) ->
     self.pretype_prod self (na, bk, t, c) ?loc ~flags tycon env sigma
-  | GLetIn (na, b, t, c) ->
+  | GLetIn (na, _, b, t, c) ->
     self.pretype_letin self (na, b, t, c) ?loc ~flags tycon env sigma
   | GCases (st, c, tm, cl) ->
     self.pretype_cases self (st, c, tm, cl) ?loc ~flags tycon env sigma
@@ -742,13 +742,13 @@ struct
     let hypnaming = if flags.program_mode then ProgramNaming vars else RenameExistingBut vars in
     let rec type_bl env sigma ctxt = function
       | [] -> sigma, ctxt
-      | (na,bk,None,ty)::bl ->
+      | (na,_,bk,None,ty)::bl ->
         let sigma, ty' = pretype_type empty_valcon env sigma ty in
         let rty' = ESorts.relevance_of_sort sigma ty'.utj_type in
         let dcl = LocalAssum (make_annot na rty', ty'.utj_val) in
         let dcl', env = push_rel ~hypnaming sigma dcl env in
         type_bl env sigma (Context.Rel.add dcl' ctxt) bl
-      | (na,bk,Some bd,ty)::bl ->
+      | (na,_,bk,Some bd,ty)::bl ->
         let sigma, ty' = pretype_type empty_valcon env sigma ty in
         let rty' = ESorts.relevance_of_sort sigma ty'.utj_type in
         let sigma, bd' = pretype (mk_tycon ty'.utj_val) env sigma bd in
@@ -1531,7 +1531,7 @@ let path_convertible env sigma cl p q =
   let mkGRef ref          = DAst.make @@ Glob_term.GRef(ref,None) in
   let mkGVar id           = DAst.make @@ Glob_term.GVar(id) in
   let mkGApp(rt,rtl)      = DAst.make @@ Glob_term.GApp(rt,rtl) in
-  let mkGLambda(n,t,b)    = DAst.make @@ Glob_term.GLambda(n,Explicit,t,b) in
+  let mkGLambda(n,t,b)    = DAst.make @@ Glob_term.GLambda(n,None,Explicit,t,b) in
   let mkGSort u           = DAst.make @@ Glob_term.GSort u in
   let mkGHole ()          = DAst.make @@ Glob_term.GHole (GBinderType Anonymous) in
   let path_to_gterm p =
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index dbd6f25942ff5..7f0934c9c0a27 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -198,6 +198,15 @@ let tag_var = tag Tag.variable
     | CQVar qid -> tag_type (pr_qualid qid)
     | CRawQVar q -> (* TODO names *) tag_type (Sorts.QVar.raw_pr q)
 
+  let pr_relevance = function
+    | CRelevant -> str "Relevant"
+    | CIrrelevant -> str "Irrelevant"
+    | CRelevanceVar q -> pr_qvar_expr q
+
+  let pr_relevance_info = function
+    | None -> mt()
+    | Some r -> str "(* " ++ pr_relevance r ++ str " *) "
+
   let pr_quality_expr q = match q with
     | CQConstant q -> tag_type (Sorts.Quality.Constants.pr q)
     | CQualVar q -> pr_qvar_expr q
@@ -423,8 +432,8 @@ let tag_var = tag Tag.variable
   let begin_of_binder l_bi =
     let b_loc l = fst (Option.cata Loc.unloc (0,0) l) in
     match l_bi with
-    | CLocalDef({loc},_,_) -> b_loc loc
-    | CLocalAssum({loc}::_,_,_) -> b_loc loc
+    | CLocalDef({loc},_,_,_) -> b_loc loc
+    | CLocalAssum({loc}::_,_,_,_) -> b_loc loc
     | CLocalPattern{loc} -> b_loc loc
     | _ -> assert false
 
@@ -444,16 +453,17 @@ let tag_var = tag Tag.variable
       | NonMaxImplicit -> str"[" ++ p ++ str"]"
       | MaxImplicit -> (str"{" ++ p ++ str"}")
 
-  let pr_binder many pr (nal,k,t) =
+  let pr_binder many pr (nal,r,k,t) =
+    let r = pr_relevance_info r in
     match k with
       | Generalized (b', t') ->
         begin match nal with
           |[{loc; v=Anonymous}] ->
             hov 1 (str"`" ++ (surround_impl b'
-                                ((if t' then str "!" else mt ()) ++ pr t)))
+                                (r ++ (if t' then str "!" else mt ()) ++ pr t)))
           |[{loc; v=Name id}] ->
             hov 1 (str "`" ++ (surround_impl b'
-                                 (pr_lident CAst.(make ?loc id) ++ str " : " ++
+                                 (pr_lident CAst.(make ?loc id) ++ str " : " ++ r ++
                                     (if t' then str "!" else mt()) ++ pr t)))
           |_ -> anomaly (Pp.str "List of generalized binders have always one element.")
         end
@@ -461,16 +471,16 @@ let tag_var = tag Tag.variable
         match t with
           | { CAst.v = CHole h } when is_anonymous_hole h ->
             let s = prlist_with_sep spc pr_lname nal in
-            hov 1 (surround_implicit b s)
+            hov 1 (r ++ surround_implicit b s)
           | _ ->
-            let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ pr t in
+            let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ r ++ pr t in
             hov 1 (if many then surround_impl b s else surround_implicit b s)
 
   let pr_binder_among_many withquote pr_c = function
-    | CLocalAssum (nal,k,t) ->
-      pr_binder true pr_c (nal,k,t)
-    | CLocalDef (na,c,topt) ->
-      surround (pr_lname na ++
+    | CLocalAssum (nal,r,k,t) ->
+      pr_binder true pr_c (nal,r,k,t)
+    | CLocalDef (na,r,c,topt) ->
+      surround (pr_lname na ++ pr_relevance_info r ++
                 pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++
                 str" :=" ++ spc() ++ pr_c c)
     | CLocalPattern p ->
@@ -482,8 +492,8 @@ let tag_var = tag Tag.variable
   let pr_delimited_binders kw sep withquote pr_c bl =
     let n = begin_of_binders bl in
     match bl with
-      | [CLocalAssum (nal,k,t)] ->
-        kw n ++ pr_binder false pr_c (nal,k,t)
+      | [CLocalAssum (nal,r,k,t)] ->
+        kw n ++ pr_binder false pr_c (nal,r,k,t)
       | (CLocalAssum _ | CLocalPattern _ | CLocalDef _) :: _ as bdl ->
         kw n ++ pr_undelimited_binders sep withquote pr_c bdl
       | [] -> anomaly (Pp.str "The ast is malformed, found lambda/prod without proper binders.")
@@ -507,8 +517,8 @@ let tag_var = tag Tag.variable
         match ro with
           | CStructRec { v = id } ->
             let names_of_binder = function
-              | CLocalAssum (nal,_,_) -> nal
-              | CLocalDef (_,_,_) -> []
+              | CLocalAssum (nal,_,_,_) -> nal
+              | CLocalDef (_,_,_,_) -> []
               | CLocalPattern _ -> assert false
             in let ids = List.flatten (List.map names_of_binder bl) in
                if List.length ids > 1 then
@@ -521,11 +531,11 @@ let tag_var = tag Tag.variable
             match id with None -> mt() | Some id -> brk (1,1) ++ pr_lident id ++
               (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
 
-  let pr_fixdecl pr prd lev_after kw dangling_with_for ({v=id},ro,bl,t,c) =
+  let pr_fixdecl pr prd lev_after kw dangling_with_for ({v=id},_,ro,bl,t,c) =
     let annot = pr_guard_annot (pr no_after lsimpleconstr) bl ro in
     pr_recursive_decl pr prd lev_after kw dangling_with_for id bl annot t c
 
-  let pr_cofixdecl pr prd lev_after kw dangling_with_for ({v=id},bl,t,c) =
+  let pr_cofixdecl pr prd lev_after kw dangling_with_for ({v=id},_,bl,t,c) =
     pr_recursive_decl pr prd lev_after kw dangling_with_for id bl (mt()) t c
 
   let pr_recursive lev_after kw pr_decl id = function
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 57732a2a172ff..8c79e3116f9cf 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -419,9 +419,9 @@ let match_goals ot nt =
     in
     let local_binder_expr ogname exp exp2 =
       match exp, exp2 with
-      | CLocalAssum (nal,bk,ty), CLocalAssum(nal2,bk2,ty2) ->
+      | CLocalAssum (nal,_,bk,ty), CLocalAssum(nal2,_,bk2,ty2) ->
         constr_expr ogname ty ty2
-      | CLocalDef (n,c,t), CLocalDef (n2,c2,t2) ->
+      | CLocalDef (n,_,c,t), CLocalDef (n2,_,c2,t2) ->
         constr_expr ogname c c2;
         constr_expr_opt ogname t t2
       | CLocalPattern p, CLocalPattern p2 ->
@@ -441,14 +441,14 @@ let match_goals ot nt =
       | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)")
     in
     let fix_expr ogname exp exp2 =
-      let (l,ro,lb,ce1,ce2), (l2,ro2,lb2,ce12,ce22) = exp,exp2 in
+      let (l,_,ro,lb,ce1,ce2), (l2,_,ro2,lb2,ce12,ce22) = exp,exp2 in
         Option.iter2 (recursion_order_expr ogname) ro ro2;
         iter2 (local_binder_expr ogname) lb lb2;
         constr_expr ogname ce1 ce12;
         constr_expr ogname ce2 ce22
     in
     let cofix_expr ogname exp exp2 =
-      let (l,lb,ce1,ce2), (l2,lb2,ce12,ce22) = exp,exp2 in
+      let (l,_,lb,ce1,ce2), (l2,_,lb2,ce12,ce22) = exp,exp2 in
         iter2 (local_binder_expr ogname) lb lb2;
         constr_expr ogname ce1 ce12;
         constr_expr ogname ce2 ce22
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 7a327e15f7e44..7ea36092e7fe2 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -263,9 +263,9 @@ let mkGHole = DAst.make @@
         Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Define false;
   })
 let mkGProd id c1 c2 = DAst.make @@
-  GProd (Name (Id.of_string id), Explicit, c1, c2)
+  GProd (Name (Id.of_string id), None, Explicit, c1, c2)
 let mkGArrow c1 c2 = DAst.make @@
-  GProd (Anonymous, Explicit, c1, c2)
+  GProd (Anonymous, None, Explicit, c1, c2)
 let mkGVar id = DAst.make @@ GVar (Id.of_string id)
 let mkGPatVar id = DAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id))
 let mkGRef r = DAst.make @@ GRef (Lazy.force r, None)
diff --git a/test-suite/output/DebugRelevances.out b/test-suite/output/DebugRelevances.out
new file mode 100644
index 0000000000000..ded81fa1e32c5
--- /dev/null
+++ b/test-suite/output/DebugRelevances.out
@@ -0,0 +1,42 @@
+foo@{u} =
+fun (A : (* Relevant *) Type) (a : (* Relevant *) A) => a
+     : forall A : (* Relevant *) Type, A -> A
+
+Arguments foo A%type_scope a
+foo'@{} =
+fun (A : (* Relevant *) Prop) (a : (* Relevant *) A) => a
+     : forall A : (* Relevant *) Prop, A -> A
+
+Arguments foo' A%type_scope a
+bar@{} =
+fun (A : (* Relevant *) SProp) (a : (* Irrelevant *) A) => a
+     : forall A : (* Relevant *) SProp, A -> A
+
+Arguments bar A%type_scope a
+baz@{s | u} =
+fun (A : (* Relevant *) Type) (a : (* s *) A) => a
+     : forall A : (* Relevant *) Type, A -> A
+
+Arguments baz A%type_scope a
+1 goal
+  
+  f := fun (A : (* Relevant *) Type) (_ : (* α3 *) A) => A
+   : forall (A : (* Relevant *) Type) (_ : (* α3 *) A), Type
+  ============================
+  True
+1 goal
+  
+  f := fun (A : (* Relevant *) Type) (_ : (* Relevant *) A) => A
+   : forall (A : (* Relevant *) Type) (_ : (* Relevant *) A), Type
+  ============================
+  True
+let x := 0 in x
+     : nat
+fix f (n : (* Relevant *) nat) : nat := 0
+     : nat -> nat
+match 0 with
+| 0 | _ => 0
+end
+     : nat
+fun v : (* Relevant *) R => p v
+     : R -> nat
diff --git a/test-suite/output/DebugRelevances.v b/test-suite/output/DebugRelevances.v
new file mode 100644
index 0000000000000..5b13636bf937a
--- /dev/null
+++ b/test-suite/output/DebugRelevances.v
@@ -0,0 +1,39 @@
+
+Set Universe Polymorphism.
+Set Printing Relevance Marks.
+
+Definition foo (A:Type) (a:A) := a.
+Definition foo' (A:Prop) (a:A) := a.
+Definition bar (A:SProp) (a:A) := a.
+Definition baz@{s|u|} (A:Type@{s|u}) (a:A) := a.
+
+Print foo.
+Print foo'.
+Print bar.
+Print baz.
+
+Inductive sFalse : SProp := .
+
+Goal True.
+  Unset Printing Notations. (* arrow notation has no binder so relevance isn't printed *)
+  pose (f:=fun A (a:A) => A).
+  Show.
+  let _ := constr:(f nat) in idtac.
+  Show.
+Abort.
+Set Printing Notations.
+
+(* TODO print relevance of letin *)
+Check let x := 0 in x.
+
+(* TODO print relevance of fixpoints (should be fix f (* Relevant *) ...) *)
+Check fix f (n:nat) := 0.
+
+
+(* TODO print case relevance *)
+Check match 0 with 0 | _ => 0 end.
+
+(* TODO print primitive projection relevance *)
+Set Primitive Projections.
+Record R := { p : nat }.
+Check fun v => v.(p).
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 070131778df90..ddd3260845ec1 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -54,9 +54,9 @@ let protect_pattern_in_binder bl c ctypopt =
     let loc = Loc.merge_opt c.CAst.loc t.CAst.loc in
     let c = CAst.make ?loc @@ Constrexpr.CCast (c, Some Constr.DEFAULTcast, t) in
     let loc = match List.hd bl with
-      | Constrexpr.CLocalAssum (a::_,_,_) | Constrexpr.CLocalDef (a,_,_) -> a.CAst.loc
+      | Constrexpr.CLocalAssum (a::_,_,_,_) | Constrexpr.CLocalDef (a,_,_,_) -> a.CAst.loc
       | Constrexpr.CLocalPattern {CAst.loc} -> loc
-      | Constrexpr.CLocalAssum ([],_,_) -> assert false in
+      | Constrexpr.CLocalAssum ([],_,_,_) -> assert false in
     let apply_under_binders f env evd c =
       let rec aux env evd c =
         let open Constr in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 640817790df62..ffdc8b391d8eb 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -313,9 +313,9 @@ let adjust_rec_order ~structonly binders rec_order =
   let rec_order = Option.map (fun rec_order ->
       let open Constrexpr in
       match binders, rec_order with
-      | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+      | [CLocalAssum([{ CAst.v = Name x }],_,_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
         CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
-      | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+      | [CLocalDef({ CAst.v = Name x },_,_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
         CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
       | _, x -> x) rec_order
   in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 7fa830dd260fb..dda7f1f1f35be 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -99,8 +99,8 @@ let rec check_type_conclusion ind =
     (* should have been made flexible *)
     assert false
   | GSort (UNamed _) -> true
-  | GProd ( _, _, _, e)
-  | GLetIn (_, _, _, e) ->
+  | GProd (_, _, _, _, e)
+  | GLetIn (_, _, _, _, e) ->
     check_type_conclusion e
   | _ -> false
 
@@ -110,13 +110,13 @@ let rec make_anonymous_conclusion_flexible ind =
   | GSort (UAnonymous {rigid=UnivRigid}) ->
     Some (DAst.make ?loc:ind.loc (GSort (UAnonymous {rigid=UnivFlexible true})))
   | GSort (UNamed _) -> None
-  | GProd (a, b, c, e) -> begin match make_anonymous_conclusion_flexible e with
+  | GProd (a, b, c, d, e) -> begin match make_anonymous_conclusion_flexible e with
       | None -> None
-      | Some e -> Some (DAst.make ?loc:ind.loc (GProd (a, b, c, e)))
+      | Some e -> Some (DAst.make ?loc:ind.loc (GProd (a, b, c, d, e)))
     end
-  | GLetIn (a, b, c, e) -> begin match make_anonymous_conclusion_flexible e with
+  | GLetIn (a, b, c, d, e) -> begin match make_anonymous_conclusion_flexible e with
       | None -> None
-      | Some e -> Some (DAst.make ?loc:ind.loc (GLetIn (a, b, c, e)))
+      | Some e -> Some (DAst.make ?loc:ind.loc (GLetIn (a, b, c, d, e)))
     end
   | _ -> None
 
@@ -441,9 +441,9 @@ match user_template, univ_entry with
     else Monomorphic_ind_entry, uctx
 
 let check_param = function
-| CLocalDef (na, _, _) -> check_named na
-| CLocalAssum (nas, Default _, _) -> List.iter check_named nas
-| CLocalAssum (nas, Generalized _, _) -> ()
+| CLocalDef (na, _, _, _) -> check_named na
+| CLocalAssum (nas, _, Default _, _) -> List.iter check_named nas
+| CLocalAssum (nas, _, Generalized _, _) -> ()
 | CLocalPattern {CAst.loc} ->
   Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed here")
 
@@ -720,7 +720,7 @@ end
 
 let rec count_binder_expr = function
   | [] -> 0
-  | CLocalAssum(l,_,_) :: rest -> List.length l + count_binder_expr rest
+  | CLocalAssum(l,_,_,_) :: rest -> List.length l + count_binder_expr rest
   | CLocalDef _ :: rest -> 1 + count_binder_expr rest
   | CLocalPattern {CAst.loc} :: _ ->
     Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed here")
diff --git a/vernac/record.ml b/vernac/record.ml
index f0cb29feb7b08..a91fad3075cf0 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -95,9 +95,9 @@ let error_parameters_must_be_named bk {CAst.loc; v=name} =
   | _ -> ()
 
 let check_parameters_must_be_named = function
-  | CLocalDef (b, _, _) ->
+  | CLocalDef (b, _, _, _) ->
     error_parameters_must_be_named default_binder_kind b
-  | CLocalAssum (ls, bk, _ce) ->
+  | CLocalAssum (ls, _, bk, _ce) ->
     List.iter (error_parameters_must_be_named bk) ls
   | CLocalPattern {CAst.loc} ->
     Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed in record parameters")