Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.

15 files changed, 205 insertions, 152 deletions

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index b5cc74b594..3773bc9c88 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -21,6 +21,7 @@ open CErrors
 open Util
 open Names
 open Constr
+open Context
 open Declarations
 open Mod_subst
 open Globnames
@@ -238,8 +239,9 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
        Array.fold_left (fun accu oib ->
           let pspecif = Univ.in_punivs (mib, oib) in
           let ind_type = Inductive.type_of_inductive global_env pspecif in
+          let indr = oib.mind_relevant in
           let ind_name = Name oib.mind_typename in
-          Context.Rel.add (Context.Rel.Declaration.LocalAssum (ind_name, ind_type)) accu)
+          Context.Rel.add (Context.Rel.Declaration.LocalAssum (make_annot ind_name indr, ind_type)) accu)
           Context.Rel.empty mib.mind_packets
      in
      (* For each inductive, collects references in their arity and in the type
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 868a6ed3e9..528829f3a5 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -16,6 +16,7 @@ open Util
 open Pp
 open Term
 open Constr
+open Context
 open Vars
 open Termops
 open Declarations
@@ -144,7 +145,7 @@ let build_beq_scheme mode kn =
   in
   (* construct the "fun A B ... N, eqA eqB eqC ... N => fixpoint" part *)
   let create_input c =
-    let myArrow u v = mkArrow u (lift 1 v)
+    let myArrow u v = mkArrow u Sorts.Relevant (lift 1 v)
     and eqName = function
         | Name s -> Id.of_string ("eq_"^(Id.to_string s))
         | Anonymous -> Id.of_string "eq_A"
@@ -161,14 +162,16 @@ let build_beq_scheme mode kn =
           ( fun a b decl -> (* mkLambda(n,b,a) ) *)
                 (* here I leave the Naming thingy so that the type of
                   the function is more readable for the user *)
-                mkNamedLambda (eqName (RelDecl.get_name decl)) b a )
+                mkNamedLambda (map_annot eqName (RelDecl.get_annot decl)) b a )
                 c (List.rev eqs_typ) lnamesparrec
        in
         List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *)
-          (* Same here , hoping the auto renaming will do something good ;)  *)
-          mkNamedLambda
-                (match RelDecl.get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
-                (RelDecl.get_type decl)  a) eq_input lnamesparrec
+           (* Same here , hoping the auto renaming will do something good ;)  *)
+           let x = map_annot
+               (function Name s -> s | Anonymous -> Id.of_string "A")
+               (RelDecl.get_annot decl)
+           in
+          mkNamedLambda x (RelDecl.get_type decl)  a) eq_input lnamesparrec
  in
  let make_one_eq cur =
   let u = Univ.Instance.empty in
@@ -251,8 +254,8 @@ let build_beq_scheme mode kn =
   in
   (* construct the predicate for the Case part*)
   let do_predicate rel_list n =
-     List.fold_left (fun a b -> mkLambda(Anonymous,b,a))
-      (mkLambda (Anonymous,
+     List.fold_left (fun a b -> mkLambda(make_annot Anonymous Sorts.Relevant,b,a))
+      (mkLambda (make_annot Anonymous Sorts.Relevant,
                  mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
                  (bb ())))
       (List.rev rettyp_l) in
@@ -260,7 +263,8 @@ let build_beq_scheme mode kn =
   (* do the [| C1 ... =>  match Y with ... end
                ...
                Cn => match Y with ... end |]  part *)
-    let ci = make_case_info env (fst ind) MatchStyle in
+    let rci = Sorts.Relevant in (* TODO relevance *)
+    let ci = make_case_info env (fst ind) rci MatchStyle in
     let constrs n = get_constructors env (make_ind_family (ind,
       Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in
     let constrsi = constrs (3+nparrec) in
@@ -296,32 +300,32 @@ let build_beq_scheme mode kn =
                           (Array.sub eqs 1 (nb_cstr_args - 1))
                   )
    		  in
-		    (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) cc
+                    (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) cc
                     (constrsj.(j).cs_args)
 		)
 	      else ar2.(j) <- (List.fold_left (fun a decl ->
-                        mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (ff ())  (constrsj.(j).cs_args) )
-	    done;
+                        mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) (ff ())  (constrsj.(j).cs_args) )
+            done;
 
-	  ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a))
+          ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
 			(mkCase (ci,do_predicate rel_list nb_cstr_args,
 				  mkVar (Id.of_string "Y") ,ar2))
 			 (constrsi.(i).cs_args))
-	done;
-        mkNamedLambda (Id.of_string "X") (mkFullInd ind (nb_ind-1+1))  (
-          mkNamedLambda (Id.of_string "Y") (mkFullInd ind (nb_ind-1+2))  (
+        done;
+        mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1))  (
+          mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2))  (
  	    mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))),
         !eff
     in (* build_beq_scheme *)
-    let names = Array.make nb_ind Anonymous and
+    let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
         types = Array.make nb_ind mkSet and
         cores = Array.make nb_ind mkSet in
     let eff = ref Safe_typing.empty_private_constants in
     let u = Univ.Instance.empty in
     for i=0 to (nb_ind-1) do
-        names.(i) <- Name (Id.of_string (rec_name i));
-	types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0)
-                     (mkArrow (mkFullInd ((kn,i),u) 1) (bb ()));
+        names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant;
+        types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant
+                     (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ()));
         let c, eff' = make_one_eq i in
         cores.(i) <- c;
         eff := Safe_typing.concat_private eff' !eff
@@ -562,34 +566,39 @@ let compute_bl_goal ind lnamesparrec nparrec =
     let x = next_ident_away (Id.of_string "x") avoid and
         y = next_ident_away (Id.of_string "y") avoid in
       let bl_typ = List.map (fun (s,seq,_,_) ->
-        mkNamedProd x (mkVar s) (
-            mkNamedProd y (mkVar s) (
+        mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
+            mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
               mkArrow
                ( mkApp(eq (),[|bb (); mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt () |]))
+               Sorts.Relevant
                ( mkApp(eq (),[|mkVar s;mkVar x;mkVar y|]))
           ))
         ) list_id in
       let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
-        mkNamedProd sbl b a
+        mkNamedProd (make_annot sbl Sorts.Relevant) b a
       ) c (List.rev list_id) (List.rev bl_typ) in
       let eqs_typ = List.map (fun (s,_,_,_) ->
-          mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(bb ())))
+          mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,(bb ())))
           ) list_id in
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
-        mkNamedProd seq b a
+        mkNamedProd (make_annot seq Sorts.Relevant) b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
-      List.fold_left (fun a decl -> mkNamedProd
-                (match RelDecl.get_name decl with Name s -> s | Anonymous -> next_ident_away (Id.of_string "A") avoid)
-                (RelDecl.get_type decl) a) eq_input lnamesparrec
+    List.fold_left (fun a decl ->
+        let x = map_annot
+            (function Name s -> s | Anonymous -> next_ident_away (Id.of_string "A") avoid)
+            (RelDecl.get_annot decl)
+        in
+        mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
     in
       let n = next_ident_away (Id.of_string "x") avoid and
           m = next_ident_away (Id.of_string "y") avoid in
       let u = Univ.Instance.empty in
      create_input (
-        mkNamedProd n (mkFullInd (ind,u) nparrec) (
-          mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
+        mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
+          mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
             mkArrow
               (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|]))
+              Sorts.Relevant
               (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
         ))), eff
 
@@ -706,34 +715,40 @@ let compute_lb_goal ind lnamesparrec nparrec =
       let x = next_ident_away (Id.of_string "x") avoid and
           y = next_ident_away (Id.of_string "y") avoid in
       let lb_typ = List.map (fun (s,seq,_,_) ->
-        mkNamedProd x (mkVar s) (
-            mkNamedProd y (mkVar s) (
+        mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
+            mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
               mkArrow
-               ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
-               ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
+                ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
+                Sorts.Relevant
+                ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
           ))
         ) list_id in
       let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b ->
-        mkNamedProd slb b a
+        mkNamedProd (make_annot slb Sorts.Relevant) b a
       ) c (List.rev list_id) (List.rev lb_typ) in
       let eqs_typ = List.map (fun (s,_,_,_) ->
-          mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb))
+          mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,
+                 mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,bb))
           ) list_id in
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
-        mkNamedProd seq b a
+        mkNamedProd (make_annot seq Sorts.Relevant) b a
       ) lb_input (List.rev list_id) (List.rev eqs_typ) in
-      List.fold_left (fun a decl -> mkNamedProd
-                (match (RelDecl.get_name decl) with Name s -> s | Anonymous ->  Id.of_string "A")
-                (RelDecl.get_type decl)  a) eq_input lnamesparrec
+      List.fold_left (fun a decl ->
+          let x = map_annot
+              (function Name s -> s | Anonymous -> Id.of_string "A")
+              (RelDecl.get_annot decl)
+          in
+          mkNamedProd x (RelDecl.get_type decl)  a) eq_input lnamesparrec
     in
       let n = next_ident_away (Id.of_string "x") avoid and
           m = next_ident_away (Id.of_string "y") avoid in
       let u = Univ.Instance.empty in
       create_input (
-        mkNamedProd n (mkFullInd (ind,u) nparrec) (
-          mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
+        mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
+          mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
             mkArrow
               (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|]))
+              Sorts.Relevant
               (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
         ))), eff
 
@@ -835,45 +850,51 @@ let compute_dec_goal ind lnamesparrec nparrec =
       let x = next_ident_away (Id.of_string "x") avoid and
           y = next_ident_away (Id.of_string "y") avoid in
       let lb_typ = List.map (fun (s,seq,_,_) ->
-        mkNamedProd x (mkVar s) (
-            mkNamedProd y (mkVar s) (
+        mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
+            mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
               mkArrow
-               ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
-               ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
+                ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
+                Sorts.Relevant
+                ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
           ))
         ) list_id in
       let bl_typ = List.map (fun (s,seq,_,_) ->
-        mkNamedProd x (mkVar s) (
-            mkNamedProd y (mkVar s) (
+        mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
+            mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
               mkArrow
-               ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
-               ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
+                ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
+                Sorts.Relevant
+                ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
           ))
         ) list_id in
 
       let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b ->
-        mkNamedProd slb b a
+        mkNamedProd (make_annot slb Sorts.Relevant) b a
       ) c (List.rev list_id) (List.rev lb_typ) in
       let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
-        mkNamedProd sbl b a
+        mkNamedProd (make_annot sbl Sorts.Relevant) b a
       ) lb_input (List.rev list_id) (List.rev bl_typ) in
 
       let eqs_typ = List.map (fun (s,_,_,_) ->
-          mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb))
+          mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,
+                 mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,bb))
           ) list_id in
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
-        mkNamedProd seq b a
+        mkNamedProd (make_annot seq Sorts.Relevant) b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
-      List.fold_left (fun a decl -> mkNamedProd
-                (match RelDecl.get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
-                (RelDecl.get_type decl) a) eq_input lnamesparrec
+      List.fold_left (fun a decl ->
+          let x = map_annot
+              (function Name s -> s | Anonymous -> Id.of_string "A")
+              (RelDecl.get_annot decl)
+          in
+          mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
     in
       let n = next_ident_away (Id.of_string "x") avoid and
           m = next_ident_away (Id.of_string "y") avoid in
         let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in
         create_input (
-          mkNamedProd n (mkFullInd ind (2*nparrec)) (
-            mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
+          mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd ind (2*nparrec)) (
+            mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) (
               mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|])
           )
         )
diff --git a/vernac/class.ml b/vernac/class.ml
index a6b3242cae..0837beccee 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -14,6 +14,7 @@ open Pp
 open Names
 open Term
 open Constr
+open Context
 open Vars
 open Termops
 open Entries
@@ -188,14 +189,14 @@ let build_id_coercion idf_opt source poly =
   let lams,t = decompose_lam_assum c in
   let val_f =
     it_mkLambda_or_LetIn
-      (mkLambda (Name Namegen.default_dependent_ident,
+      (mkLambda (make_annot (Name Namegen.default_dependent_ident) Sorts.Relevant,
 		 applistc vs (Context.Rel.to_extended_list mkRel 0 lams),
 		 mkRel 1))
        lams
   in
   let typ_f =
     List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d)
-      (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list mkRel 0 lams), lift 1 t))
+      (mkProd (make_annot Anonymous Sorts.Relevant, applistc vs (Context.Rel.to_extended_list mkRel 0 lams), lift 1 t))
       lams
   in
   (* juste pour verification *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 4664df3182..1981e24ae4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -352,8 +352,8 @@ let named_of_rel_context l =
       (fun decl (subst, ctx) ->
         let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
 	let d = match decl with
-	  | LocalAssum (_,t) -> id, None, substl subst t
-	  | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
+          | LocalAssum (_,t) -> id, None, substl subst t
+          | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
 	  (mkVar id :: subst, d :: ctx))
       l ([], [])
   in ctx
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 35d8be5c56..37a33daf8f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -13,6 +13,7 @@ open Util
 open Vars
 open Declare
 open Names
+open Context
 open Globnames
 open Constrexpr_ops
 open Constrintern
@@ -148,8 +149,9 @@ let do_assumptions ~program_mode kind nl l =
   (* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
   let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
     let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in
+    let r = Retyping.relevance_of_type env sigma t in
     let env =
-      EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
+      EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in
     let ienv = List.fold_right (fun {CAst.v=id} ienv ->
       let impls = compute_internalization_data env sigma Variable t imps in
       Id.Map.add id impls ienv) idl ienv in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 5229d9e8e8..2f00b41b7c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -12,6 +12,7 @@ open Pp
 open CErrors
 open Util
 open Constr
+open Context
 open Vars
 open Termops
 open Declare
@@ -126,7 +127,9 @@ let interp_fix_context ~program_mode ~cofix env sigma fix =
   sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
 let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
-  interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type
+  let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type in
+  let r = Retyping.relevance_of_type env sigma c in
+  sigma, (c, r, impl)
 
 let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl =
   let open EConstr in
@@ -137,9 +140,9 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
 
-let prepare_recursive_declaration fixnames fixtypes fixdefs =
+let prepare_recursive_declaration fixnames fixrs fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
-  let names = List.map (fun id -> Name id) fixnames in
+  let names = List.map2 (fun id r -> make_annot (Name id) r) fixnames fixrs in
   (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
 
 (* Jump over let-bindings. *)
@@ -158,7 +161,7 @@ let compute_possible_guardness_evidences (ctx,_,recindex) =
       List.interval 0 (Context.Rel.nhyps ctx - 1)
 
 type recursive_preentry =
-  Id.t list * constr option list * types list
+  Id.t list * Sorts.relevance list * constr option list * types list
 
 (* Wellfounded definition *)
 
@@ -188,8 +191,8 @@ let interp_recursive ~program_mode ~cofix fixl notations =
     on_snd List.split3 @@
       List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
-  let sigma, (fixccls,fixcclimps) =
-    on_snd List.split @@
+  let sigma, (fixccls,fixrs,fixcclimps) =
+    on_snd List.split3 @@
       List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in
@@ -208,8 +211,8 @@ let interp_recursive ~program_mode ~cofix fixl notations =
                Typing.solve_evars env sigma app
              with e when CErrors.noncritical e -> sigma, t
            in
-           sigma, LocalAssum (id,fixprot) :: env'
-         else sigma, LocalAssum (id,t) :: env')
+           sigma, LocalAssum (make_annot id Sorts.Relevant,fixprot) :: env'
+         else sigma, LocalAssum (make_annot id Sorts.Relevant,t) :: env')
       (sigma,[]) fixnames fixtypes
   in
   let env_rec = push_named_context rec_sign env in
@@ -232,19 +235,19 @@ let interp_recursive ~program_mode ~cofix fixl notations =
   let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
   (* Build the fix declaration block *)
-  (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
+  (env,rec_sign,decl,sigma), (fixnames,fixrs,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
 
-let check_recursive isfix env evd (fixnames,fixdefs,_) =
+let check_recursive isfix env evd (fixnames,_,fixdefs,_) =
   if List.for_all Option.has_some fixdefs then begin
     let fixdefs = List.map Option.get fixdefs in
     check_mutuality env evd isfix (List.combine fixnames fixdefs)
   end
 
-let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) =
+let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
   check_evars_are_solved ~program_mode:false env evd;
   let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
   let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
-  Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes)
+  Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
 
 let interp_fixpoint ~cofix l ntns =
   let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in
@@ -252,7 +255,7 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -267,7 +270,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
-    let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+    let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
     let env = Global.env() in
     let indexes = search_guard env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
@@ -287,7 +290,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
 
-let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -302,7 +305,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
-    let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+    let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
     let vars = Vars.universes_of_constr (List.hd fixdecls) in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 338dfa5ef5..9bcb53697b 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -51,7 +51,7 @@ val interp_recursive :
   (* env / signature / univs / evar_map *)
   (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
-  (Id.t list * EConstr.constr option list * EConstr.types list) *
+  (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
   (* ctx per mutual def / implicits / struct annotations *)
   (EConstr.rel_context * Impargs.manual_explicitation list * int option) list
 
@@ -69,7 +69,7 @@ val extract_cofixpoint_components :
     structured_fixpoint_expr list * decl_notation list
 
 type recursive_preentry =
-  Id.t list * constr option list * types list
+  Id.t list * Sorts.relevance list * constr option list * types list
 
 val interp_fixpoint :
   cofix:bool ->
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index e71946e8b8..8b8307c14a 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -13,6 +13,7 @@ open CErrors
 open Sorts
 open Util
 open Constr
+open Context
 open Environ
 open Declare
 open Names
@@ -70,9 +71,9 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
   | c -> c
   )
 
-let push_types env idl tl =
-  List.fold_left2 (fun env id t -> EConstr.push_rel (LocalAssum (Name id,t)) env)
-    env idl tl
+let push_types env idl rl tl =
+  List.fold_left3 (fun env id r t -> EConstr.push_rel (LocalAssum (make_annot (Name id) r,t)) env)
+    env idl rl tl
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
@@ -152,7 +153,7 @@ let interp_ind_arity env sigma ind =
     user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
   | s ->
     let concl = if pseudo_poly then Some s else None in
-    sigma, (t, concl, impls)
+    sigma, (t, Retyping.relevance_of_sort s,  concl, impls)
 
 let interp_cstrs env sigma impls mldata arity ind =
   let cnames,ctyps = List.split ind.ind_lc in
@@ -183,7 +184,7 @@ let sup_list min = List.fold_left Univ.sup min
 let extract_level env evd min tys =
   let sorts = List.map (fun ty ->
     let ctx, concl = Reduction.dest_prod_assum env ty in
-      sign_level env evd (LocalAssum (Anonymous, concl) :: ctx)) tys
+      sign_level env evd (LocalAssum (make_annot Anonymous Sorts.Relevant, concl) :: ctx)) tys
   in sup_list min sorts
 
 let is_flexible_sort evd u =
@@ -370,15 +371,15 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
 
   (* Interpret the arities *)
   let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in
+  let arities, relevances, arityconcl, indimpls = List.split4 arities in
 
-  let fullarities = List.map (fun (c, _, _) -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
-  let env_ar = push_types env_uparams indnames fullarities in
+  let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
+  let env_ar = push_types env_uparams indnames relevances fullarities in
   let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
 
   (* Compute interpretation metadatas *)
-  let indimpls = List.map (fun (_, _, impls) -> userimpls @
-    lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
-  let arities = List.map pi1 arities and arityconcl = List.map pi2 arities in
+  let indimpls = List.map (fun impls -> userimpls @
+    lift_implicits (Context.Rel.nhyps ctx_params) impls) indimpls in
   let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
   let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
@@ -407,7 +408,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in
   let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in
   let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in
-  let env_ar = push_types env0 indnames fullarities in
+  let env_ar = push_types env0 indnames relevances fullarities in
   let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
 
   (* Try further to solve evars, and instantiate them *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index ae77cf12e5..ad7c65b70c 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -12,6 +12,7 @@ open Pp
 open CErrors
 open Util
 open Constr
+open Context
 open Entries
 open Vars
 open Declare
@@ -41,7 +42,7 @@ let well_founded sigma = init_constant sigma (lib_ref "core.wf.well_founded")
 let mkSubset sigma name typ prop =
   let open EConstr in
   let sigma, app_h = Evarutil.new_global sigma (delayed_force build_sigma).typ in
-  sigma, mkApp (app_h, [| typ; mkLambda (name, typ, prop) |])
+  sigma, mkApp (app_h, [| typ; mkLambda (make_annot name Sorts.Relevant, typ, prop) |])
 
 let make_qref s = qualid_of_string s
 let lt_ref = make_qref "Init.Peano.lt"
@@ -58,7 +59,7 @@ let rec telescope sigma l =
         List.fold_left
           (fun (sigma, ty, tys, (k, constr)) decl ->
             let t = RelDecl.get_type decl in
-            let pred = mkLambda (RelDecl.get_name decl, t, ty) in
+            let pred = mkLambda (RelDecl.get_annot decl, t, ty) in
             let sigma, ty = Evarutil.new_global sigma (lib_ref "core.sigT.type") in
             let sigma, intro = Evarutil.new_global sigma (lib_ref "core.sigT.intro") in
             let sigty = mkApp (ty, [|t; pred|]) in
@@ -73,7 +74,7 @@ let rec telescope sigma l =
           let sigma, p2 = Evarutil.new_global sigma (lib_ref "core.sigT.proj2") in
           let proj1 = applist (p1, [t; pred; prev]) in
           let proj2 = applist (p2, [t; pred; prev]) in
-            (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
+            (sigma, lift 1 proj2, LocalDef (get_annot decl, proj1, t) :: subst))
         (List.rev tys) tl (sigma, mkRel 1, [])
       in sigma, ty, (LocalDef (n, last, t) :: subst), constr
 
@@ -98,7 +99,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
   let sigma, argtyp, letbinders, make = telescope sigma binders_rel in
   let argname = Id.of_string "recarg" in
-  let arg = LocalAssum (Name argname, argtyp) in
+  let arg = LocalAssum (make_annot (Name argname) Sorts.Relevant, argtyp) in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
   let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in
@@ -135,7 +136,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let argid' = Id.of_string (Id.to_string argname ^ "'") in
   let wfarg sigma len =
     let sigma, ss_term = mkSubset sigma (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1))) in
-    sigma, LocalAssum (Name argid', ss_term)
+    sigma, LocalAssum (make_annot (Name argid') Sorts.Relevant, ss_term)
   in
   let sigma, intern_bl =
     let sigma, wfa = wfarg sigma 1 in
@@ -143,7 +144,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   in
   let _intern_env = push_rel_context intern_bl env in
   let sigma, proj = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.proj1 in
-  let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
+  let wfargpred = mkLambda (make_annot (Name argid') Sorts.Relevant, argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
   let projection = (* in wfarg :: arg :: before *)
     mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
   in
@@ -153,22 +154,23 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
      now intern_arity is in wfarg :: arg *)
   let sigma, wfa = wfarg sigma 1 in
   let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfa] in
-  let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
+  let intern_fun_binder = LocalAssum (make_annot (Name (add_suffix recname "'")) Sorts.Relevant,
+                                      intern_fun_arity_prod) in
   let sigma, curry_fun =
-    let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
+    let wfpred = mkLambda (make_annot (Name argid') Sorts.Relevant, argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
     let sigma, intro = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.intro in
     let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
     let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
     let rcurry = mkApp (rel, [| measure; lift len measure |]) in
-    let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in
+    let lam = LocalAssum (make_annot (Name (Id.of_string "recproof")) Sorts.Relevant, rcurry) in
     let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
     let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
-    sigma, LocalDef (Name recname, body, ty)
+    sigma, LocalDef (make_annot (Name recname) Sorts.Relevant, body, ty)
   in
   let fun_bl = intern_fun_binder :: [arg] in
   let lift_lets = lift_rel_context 1 letbinders in
   let sigma, intern_body =
-    let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
+    let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in
     let (r, l, impls, scopes) =
       Constrintern.compute_internalization_data env sigma
         Constrintern.Recursive full_arity impls
@@ -180,7 +182,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       ~impls:newimpls body (lift 1 top_arity)
   in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
-  let prop = mkLambda (Name argname, argtyp, top_arity_let) in
+  let prop = mkLambda (make_annot (Name argname) Sorts.Relevant, argtyp, top_arity_let) in
   (* XXX: Previous code did parallel evdref update, so possible old
      weak ordering semantics may bite here. *)
   let sigma, def =
@@ -272,7 +274,7 @@ let do_program_recursive local poly fixkind fixl ntns =
         (List.length rec_sign) def typ
     in (id, def, typ, imps, evars)
   in
-  let (fixnames,fixdefs,fixtypes) = fix in
+  let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
   let fixdefs = List.map out_def fixdefs in
   let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
@@ -281,7 +283,7 @@ let do_program_recursive local poly fixkind fixl ntns =
       (* XXX: are we allowed to have evars here? *)
       let fixtypes = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixtypes in
       let fixdefs = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixdefs in
-      let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
+      let fixdecls = Array.of_list (List.map2 (fun x r -> make_annot (Name x) r) fixnames fixrs),
         Array.of_list fixtypes,
         Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
       in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index fd5970e8ca..0e0788c470 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Namegen
 open Constr
+open Context
 open Termops
 open Environ
 open Pretype_errors
@@ -103,9 +104,9 @@ let canonize_constr sigma c =
   let dn = Name.Anonymous in
   let rec canonize_binders c =
     match EConstr.kind sigma c with
-    | Prod (_,t,b) -> mkProd(dn,t,b)
-    | Lambda (_,t,b) -> mkLambda(dn,t,b)
-    | LetIn (_,u,t,b) -> mkLetIn(dn,u,t,b)
+    | Prod (x,t,b) -> mkProd({x with binder_name=dn},t,b)
+    | Lambda (x,t,b) -> mkLambda({x with binder_name=dn},t,b)
+    | LetIn (x,u,t,b) -> mkLetIn({x with binder_name=dn},u,t,b)
     | _ -> EConstr.map sigma canonize_binders c
   in
   canonize_binders c
@@ -193,13 +194,13 @@ let rec pr_disjunction pr = function
   | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
   | [] -> assert false
 
-let explain_elim_arity env sigma ind sorts c pj okinds =
+let explain_elim_arity env sigma ind c pj okinds =
   let open EConstr in
   let env = make_all_name_different env sigma in
   let pi = pr_inductive env (fst ind) in
   let pc = pr_leconstr_env env sigma c in
   let msg = match okinds with
-  | Some(kp,ki,explanation) ->
+  | Some(sorts,kp,ki,explanation) ->
       let pki = Sorts.pr_sort_family ki in
       let pkp = Sorts.pr_sort_family kp in
       let explanation =	match explanation with
@@ -262,7 +263,7 @@ let explain_ill_formed_branch env sigma c ci actty expty =
 let explain_generalization env sigma (name,var) j =
   let pe = pr_ne_context_of (str "In environment") env sigma in
   let pv = pr_letype_env env sigma var in
-  let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) sigma j in
+  let (pc,pt) = pr_ljudge_env (push_rel_assum (make_annot name Sorts.Relevant,var) env) sigma j in
   pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
   str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++
   str "it has type" ++ spc () ++ pt ++
@@ -414,7 +415,7 @@ let explain_not_product env sigma c =
 let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
   let pr_lconstr_env env sigma c = pr_leconstr_env env sigma c in
   let prt_name i =
-    match names.(i) with
+    match names.(i).binder_name with
         Name id -> str "Recursive definition of " ++ Id.print id
       | Anonymous -> str "The " ++ pr_nth i ++ str " definition" in
 
@@ -429,7 +430,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
   | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) ->
       let arg_env = make_all_name_different arg_env sigma in
       let called =
-        match names.(j) with
+        match names.(j).binder_name with
             Name id -> Id.print id
           | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
       let pr_db x = quote (pr_db env x) in
@@ -449,7 +450,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
 
   | NotEnoughArgumentsForFixCall j ->
       let called =
-        match names.(j) with
+        match names.(j).binder_name with
             Name id -> Id.print id
           | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
      str "Recursive call to " ++ called ++ str " has not enough arguments"
@@ -713,6 +714,9 @@ let explain_undeclared_universe env sigma l =
 let explain_disallowed_sprop () =
   Pp.(str "SProp not allowed, you need to use -allow-sprop.")
 
+let explain_bad_relevance env =
+  strbrk "Bad relevance (maybe a bugged tactic)."
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -726,8 +730,8 @@ let explain_type_error env sigma err =
       explain_bad_assumption env sigma c
   | ReferenceVariables (id,c) ->
       explain_reference_variables sigma id c
-  | ElimArity (ind, aritylst, c, pj, okinds) ->
-      explain_elim_arity env sigma ind aritylst c pj okinds
+  | ElimArity (ind, c, pj, okinds) ->
+      explain_elim_arity env sigma ind c pj okinds
   | CaseNotInductive cj ->
       explain_case_not_inductive env sigma cj
   | NumberBranches (cj, n) ->
@@ -755,6 +759,7 @@ let explain_type_error env sigma err =
   | UndeclaredUniverse l ->
      explain_undeclared_universe env sigma l
   | DisallowedSProp -> explain_disallowed_sprop ()
+  | BadRelevance -> explain_bad_relevance env
 
 let pr_position (cl,pos) =
   let clpos = match cl with
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 28ee3d184f..1e733acc59 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -228,17 +228,20 @@ let declare_one_case_analysis_scheme ind =
 let kinds_from_prop =
   [InType,rect_scheme_kind_from_prop;
    InProp,ind_scheme_kind_from_prop;
-   InSet,rec_scheme_kind_from_prop]
+   InSet,rec_scheme_kind_from_prop;
+   InSProp,sind_scheme_kind_from_prop]
 
 let kinds_from_type =
   [InType,rect_dep_scheme_kind_from_type;
    InProp,ind_dep_scheme_kind_from_type;
-   InSet,rec_dep_scheme_kind_from_type]
+   InSet,rec_dep_scheme_kind_from_type;
+   InSProp,sind_dep_scheme_kind_from_type]
 
 let nondep_kinds_from_type =
   [InType,rect_scheme_kind_from_type;
    InProp,ind_scheme_kind_from_type;
-   InSet,rec_scheme_kind_from_type]
+   InSet,rec_scheme_kind_from_type;
+   InSProp,sind_scheme_kind_from_type]
 
 let declare_one_induction_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 77f125e878..0d0732cbb4 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -330,7 +330,7 @@ let initialize_named_context_for_proof () =
   List.fold_right
     (fun d signv ->
       let id = NamedDecl.get_id d in
-      let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
+      let d = if variable_opacity id then NamedDecl.drop_body d else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
 let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook : declaration_hook option) c =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 38cdfc2d7a..9aca48f529 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -13,6 +13,7 @@ open Declare
 
 open Term
 open Constr
+open Context
 open Vars
 open Names
 open Evd
@@ -124,11 +125,11 @@ let etype_of_evar evs hyps concl =
             | LocalDef (id,c,_) ->
 		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
 		let c' = subst_vars acc 0 c' in
-		  mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
+                  mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
 		Int.Set.union s'' s',
 		Id.Set.union trans'' trans'
-	    | LocalAssum (id,_) ->
-		mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
+            | LocalAssum (id,_) ->
+                mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
     | [] ->
 	let t', s, trans = subst_evar_constr evs n mkVar concl in
 	  subst_vars acc 0 t', s, trans
@@ -479,7 +480,7 @@ let declare_definition prg =
 
 let rec lam_index n t acc =
   match Constr.kind t with
-    | Lambda (Name n', _, _) when Id.equal n n' ->
+    | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' ->
       acc
     | Lambda (_, _, b) ->
 	lam_index n b (succ acc)
@@ -508,11 +509,12 @@ let declare_mutual_definition l =
     let subs, typ = subst_prog oblsubst x in
     let env = Global.env () in
     let sigma = Evd.from_ctx x.prg_ctx in
+    let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in
     let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
     let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
     let term = EConstr.to_constr sigma term in
     let typ = EConstr.to_constr sigma typ in
-    let def = (x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) in
+    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in
     let oblsubst = List.map (fun (id, (_, c)) -> id, c) oblsubst in
     def, oblsubst
   in
@@ -522,10 +524,12 @@ let declare_mutual_definition l =
         (xdef :: defs, xobls @ obls)) l ([], [])
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixdefs, fixtypes, fiximps = List.split3 defs in
+  let fixdefs, fixrs, fixtypes, fiximps = List.split4 defs in
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
-  let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
+  let rvec = Array.of_list fixrs in
+  let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
+  let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
   let (local,poly,kind) = first.prg_kind in
   let fixnames = first.prg_deps in
   let opaque = first.prg_opaque in
diff --git a/vernac/record.ml b/vernac/record.ml
index 9f5658ecbd..6b223f845b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -17,6 +17,7 @@ open Names
 open Globnames
 open Nameops
 open Constr
+open Context
 open Vars
 open Environ
 open Declarations
@@ -66,6 +67,7 @@ let interp_fields_evars env sigma impls_env nots l =
   List.fold_left2
     (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
       let sigma, (t', impl) = interp_type_evars_impls ~program_mode:false env sigma ~impls t in
+      let r = Retyping.relevance_of_type env sigma t' in
       let sigma, b' =
         Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
                       interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
@@ -75,8 +77,8 @@ let interp_fields_evars env sigma impls_env nots l =
         | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
       in
       let d = match b' with
-	      | None -> LocalAssum (i,t')
-	      | Some b' -> LocalDef (i,b',t')
+              | None -> LocalAssum (make_annot i r,t')
+              | Some b' -> LocalDef (make_annot i r,b',t')
       in
       List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
       (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
@@ -144,8 +146,10 @@ let typecheck_params_and_fields finite def poly pl ps records =
   in
   let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in
   let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in
-  let fold accu (id, _, _, _) arity = EConstr.push_rel (LocalAssum (Name id,arity)) accu in
-  let env_ar = EConstr.push_rel_context newps (List.fold_left2 fold env0 records arities) in
+  let relevances = List.map (fun (_,s) -> Sorts.relevance_of_sort s) typs in
+  let fold accu (id, _, _, _) arity r =
+    EConstr.push_rel (LocalAssum (make_annot (Name id) r,arity)) accu in
+  let env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in
   let assums = List.filter is_local_assum newps in
   let impls_env =
     let params = List.map (RelDecl.get_name %> Name.get_id) assums in
@@ -213,12 +217,12 @@ let warning_or_error coe indsp err =
 	   strbrk " not defined.")
     | BadTypedProj (fi,ctx,te) ->
 	match te with
-	  | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) ->
+          | ElimArity (_,_,_,Some (_,_,_,NonInformativeToInformative)) ->
               (Id.print fi ++
 		strbrk" cannot be defined because it is informative and " ++
 		Printer.pr_inductive (Global.env()) indsp ++
 		strbrk " is not.")
-	  | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
+          | ElimArity (_,_,_,Some (_,_,_,StrongEliminationOnNonSmallType)) ->
 	      (Id.print fi ++
 		strbrk" cannot be defined because it is large and " ++
 		Printer.pr_inductive (Global.env()) indsp ++
@@ -284,7 +288,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
   let r = mkIndU (indsp,u) in
   let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
   let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*)
-  let x = Name binder_name in
+  let x = make_annot (Name binder_name) mip.mind_relevant in
   let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
   let primitive = 
@@ -316,18 +320,19 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
 	      else
 		let ccl = subst_projection fid subst ti in
 		let body = match decl with
-		  | LocalDef (_,ci,_) -> subst_projection fid subst ci
-		  | LocalAssum _ ->
+                  | LocalDef (_,ci,_) -> subst_projection fid subst ci
+                  | LocalAssum ({binder_relevance=rci},_) ->
 	            (* [ccl] is defined in context [params;x:rp] *)
 		    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
 		    let ccl' = liftn 1 2 ccl in
-		    let p = mkLambda (x, lift 1 rp, ccl') in
+                    let p = mkLambda (x, lift 1 rp, ccl') in
 		    let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
-		    let ci = Inductiveops.make_case_info env indsp LetStyle in
-		      mkCase (ci, p, mkRel 1, [|branch|]) 
-		in
+                    let ci = Inductiveops.make_case_info env indsp rci LetStyle in
+                    (* Record projections have no is *)
+                    mkCase (ci, p, mkRel 1, [|branch|])
+                in
 		let proj =
-	          it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
+                  it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
 		let projtyp =
                   it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
@@ -463,7 +468,9 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
   let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in
   let data =
     match fields with
-    | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->
+    | [LocalAssum ({binder_name=Name proj_name} as binder, field)
+      | LocalDef ({binder_name=Name proj_name} as binder, _, field)] when def ->
+      let binder = {binder with binder_name=Name binder_name} in
       let class_body = it_mkLambda_or_LetIn field params in
       let class_type = it_mkProd_or_LetIn arity params in
       let class_entry = 
@@ -477,11 +484,11 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       in
       let cstu = (cst, inst) in
       let inst_type = appvectc (mkConstU cstu)
-			       (Termops.rel_vect 0 (List.length params)) in
+          (Termops.rel_vect 0 (List.length params)) in
       let proj_type =
-	it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
+        it_mkProd_or_LetIn (mkProd(binder, inst_type, lift 1 field)) params in
       let proj_body =
-	it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
+        it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in
       let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
       let proj_cst = Declare.declare_constant proj_name
         (DefinitionEntry proj_entry, IsDefinition Definition)
@@ -548,12 +555,13 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
 
 let add_constant_class env cst =
   let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in
+  let r = (Environ.lookup_constant cst env).const_relevance in
   let ctx, arity = decompose_prod_assum ty in
   let tc = 
     { cl_univs = univs;
       cl_impl = ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
-      cl_props = [LocalAssum (Anonymous, arity)];
+      cl_props = [LocalAssum (make_annot Anonymous r, arity)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
       cl_unique = !typeclasses_unique
@@ -570,10 +578,11 @@ let add_inductive_class env ind =
     let env = push_rel_context ctx env in
     let inst = Univ.make_abstract_instance univs in
     let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
+    let r = Inductive.relevance_of_inductive env ind in
       { cl_univs = univs;
         cl_impl = IndRef ind;
 	cl_context = List.map (const None) ctx, ctx;
-	cl_props = [LocalAssum (Anonymous, ty)];
+        cl_props = [LocalAssum (make_annot Anonymous r, ty)];
 	cl_projs = [];
 	cl_strict = !typeclasses_strict;
 	cl_unique = !typeclasses_unique }
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d227834fcf..b9d0a27b39 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -144,8 +144,8 @@ let make_cases_aux glob_ref =
 	       | [] -> []
                | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
                | RelDecl.LocalAssum (n, _)::l ->
-		   let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
-		   Id.to_string n' :: rename (Id.Set.add n' avoid) l in
+                   let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in
+                   Id.to_string n' :: rename (Id.Set.add n' avoid) l in
 	     let al' = rename Id.Set.empty al in
 	     let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
 	     (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)