Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

14 files changed, 197 insertions, 134 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 2f2bd8d2bc..06246ef584 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -77,7 +77,7 @@ let constr_val_discr_st sigma ts t =
     | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
     | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Label(ProdLabel, [d; c])
-    | Lambda (n, d, c) -> 
+    | Lambda (n, d, c) ->
       if List.is_empty l then 
 	Label(LambdaLabel, [d; c] @ l)
       else Everything
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index bd95a62532..3ff2e3852d 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Constr
+open Context
 open EConstr
 open Hipattern
 open Tactics
@@ -19,10 +20,10 @@ module NamedDecl = Context.Named.Declaration
 
 (* Absurd *)
 
-let mk_absurd_proof coq_not t =
+let mk_absurd_proof coq_not r t =
   let id = Namegen.default_dependent_ident in
-  mkLambda (Names.Name id,mkApp(coq_not,[|t|]),
-    mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
+  mkLambda (make_annot (Names.Name id) Sorts.Relevant,mkApp(coq_not,[|t|]),
+    mkLambda (make_annot (Names.Name id) r,t,mkApp (mkRel 2,[|mkRel 1|])))
 
 let absurd c =
   Proofview.Goal.enter begin fun gl ->
@@ -31,12 +32,13 @@ let absurd c =
     let j = Retyping.get_judgment_of env sigma c in
     let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
     let t = j.Environ.utj_val in
+    let r = Sorts.relevance_of_sort j.Environ.utj_type in
     Proofview.Unsafe.tclEVARS sigma <*>
     Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.not.type")) >>= fun coqnot ->
     Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.False.type")) >>= fun coqfalse ->
     Tacticals.New.tclTHENLIST [
       elim_type coqfalse;
-      Simple.apply (mk_absurd_proof coqnot t)
+      Simple.apply (mk_absurd_proof coqnot r t)
     ]
   end
 
@@ -68,9 +70,9 @@ let contradiction_context =
 	  if is_empty_type sigma typ then
 	    simplest_elim (mkVar id)
 	  else match EConstr.kind sigma typ with
-	  | Prod (na,t,u) when is_empty_type sigma u ->
+          | Prod (na,t,u) when is_empty_type sigma u ->
              let is_unit_or_eq = match_with_unit_or_eq_type sigma t in
-	     Tacticals.New.tclORELSE
+             Tacticals.New.tclORELSE
                (match is_unit_or_eq with
                | Some _ ->
                    let hd,args = decompose_app sigma t in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 3b69d9922d..1fae4c3d9d 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -88,14 +88,27 @@ let ind_scheme_kind_from_type =
   declare_individual_scheme_object "_ind_nodep"
   (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp)
 
+let sind_scheme_kind_from_type =
+  declare_individual_scheme_object "_sind_nodep"
+  (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants)
+
 let ind_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
   (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp)
 
+let sind_dep_scheme_kind_from_type =
+  declare_individual_scheme_object "_sind" ~aux:"_sind_from_type"
+  (fun _ x -> build_induction_scheme_in_type true InSProp x, Safe_typing.empty_private_constants)
+
 let ind_scheme_kind_from_prop =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
   (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp)
 
+let sind_scheme_kind_from_prop =
+  declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop"
+  (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants)
+
+
 (* Case analysis *)
 
 let build_case_analysis_scheme_in_type dep sort ind =
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index ece4124b8b..4472792449 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -22,11 +22,14 @@ val optimize_non_type_induction_scheme :
 
 val rect_scheme_kind_from_prop : individual scheme_kind
 val ind_scheme_kind_from_prop : individual scheme_kind
+val sind_scheme_kind_from_prop : individual scheme_kind
 val rec_scheme_kind_from_prop : individual scheme_kind
 val rect_scheme_kind_from_type : individual scheme_kind
 val rect_dep_scheme_kind_from_type : individual scheme_kind
 val ind_scheme_kind_from_type : individual scheme_kind
 val ind_dep_scheme_kind_from_type : individual scheme_kind
+val sind_scheme_kind_from_type : individual scheme_kind
+val sind_dep_scheme_kind_from_type : individual scheme_kind
 val rec_scheme_kind_from_type : individual scheme_kind
 val rec_dep_scheme_kind_from_type : individual scheme_kind
 
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 6388aa2c33..e75a61d0c6 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -18,6 +18,7 @@ open Util
 open Names
 open Namegen
 open Constr
+open Context
 open EConstr
 open Declarations
 open Tactics
@@ -74,7 +75,8 @@ let generalize_right mk typ c1 c2 =
     let env = Proofview.Goal.env gl in
   Refine.refine ~typecheck:false begin fun sigma ->
     let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in
-    let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
+    let r = Retyping.relevance_of_type env sigma typ in
+    let newconcl = mkProd (make_annot na r, typ, mk typ c1 (mkRel 1)) in
     let (sigma, x) = Evarutil.new_evar env sigma ~principal:true newconcl in
     (sigma, mkApp (x, [|c2|]))
   end
@@ -123,8 +125,8 @@ let mkGenDecideEqGoal rectype ops g =
   let hypnames = pf_ids_set_of_hyps g in
   let xname    = next_ident_away idx hypnames
   and yname    = next_ident_away idy hypnames in
-  (mkNamedProd xname rectype
-     (mkNamedProd yname rectype
+  (mkNamedProd (make_annot xname Sorts.Relevant) rectype
+     (mkNamedProd (make_annot yname Sorts.Relevant) rectype
         (mkDecideEqGoal true ops
           rectype (mkVar xname) (mkVar yname))))
 
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 3c1115d056..073d66e4aa 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -51,6 +51,7 @@ open Util
 open Names
 open Term
 open Constr
+open Context
 open Vars
 open Declarations
 open Environ
@@ -66,7 +67,7 @@ module RelDecl = Context.Rel.Declaration
 
 let hid = Id.of_string "H"
 let xid = Id.of_string "X"
-let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
+let default_id_of_sort = function InSProp | InProp | InSet -> hid | InType -> xid
 let fresh env id = next_global_ident_away id Id.Set.empty
 let with_context_set ctx (b, ctx') = 
   (b, Univ.ContextSet.union ctx ctx')
@@ -80,8 +81,8 @@ let build_dependent_inductive ind (mib,mip) =
 
 let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na
 let name_assumption env = function
-| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
-| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
+| LocalAssum (na,t) -> LocalAssum (map_annot (named_hd env t) na, t)
+| LocalDef (na,c,t) -> LocalDef (map_annot (named_hd env c) na, c, t)
 
 let name_context env hyps =
   snd
@@ -202,11 +203,14 @@ let build_sym_scheme env ind =
     get_sym_eq_data env indu in
   let cstr n =
     mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect mkRel n mib.mind_params_ctxt) in
-  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let inds = snd (mind_arity mip) in
+  let varH = fresh env (default_id_of_sort inds) in
   let applied_ind = build_dependent_inductive indu specif in
+  let indr = Sorts.relevance_of_sort_family inds in
   let realsign_ind =
-    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
-  let ci = make_case_info (Global.env()) ind RegularStyle in
+    name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
+  let rci = Sorts.Relevant in (* TODO relevance *)
+  let ci = make_case_info (Global.env()) ind rci RegularStyle in
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
@@ -256,7 +260,9 @@ let build_sym_involutive_scheme env ind =
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
   let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect mkRel n paramsctxt) in
-  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let inds = snd (mind_arity mip) in
+  let indr = Sorts.relevance_of_sort_family inds in
+  let varH = fresh env (default_id_of_sort inds) in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_C =
     mkApp
@@ -264,8 +270,9 @@ let build_sym_involutive_scheme env ind =
          (Context.Rel.to_extended_vect mkRel (nrealargs+1) mib.mind_params_ctxt)
          (rel_vect (nrealargs+1) nrealargs)) in
   let realsign_ind =
-    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
-  let ci = make_case_info (Global.env()) ind RegularStyle in
+    name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
+  let rci = Sorts.Relevant in (* TODO relevance *)
+  let ci = make_case_info (Global.env()) ind rci RegularStyle in
   let c = 
     (my_it_mkLambda_or_LetIn paramsctxt
      (my_it_mkLambda_or_LetIn_name realsign_ind
@@ -368,7 +375,9 @@ let build_l2r_rew_scheme dep env ind kind =
     mkApp (mkConstructUi(indu,1),
       Array.concat [Context.Rel.to_extended_vect mkRel n paramsctxt1;
                     rel_vect p nrealargs]) in
-  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let inds = snd (mind_arity mip) in
+  let indr = Sorts.relevance_of_sort_family inds in
+  let varH = fresh env (default_id_of_sort inds) in
   let varHC = fresh env (Id.of_string "HC") in
   let varP = fresh env (Id.of_string "P") in
   let applied_ind = build_dependent_inductive indu specif in
@@ -384,9 +393,9 @@ let build_l2r_rew_scheme dep env ind kind =
         rel_vect 0 nrealargs]) in
   let realsign_P = lift_rel_context nrealargs realsign in
   let realsign_ind_P =
-    name_context env ((LocalAssum (Name varH,applied_ind_P))::realsign_P) in
+    name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind_P))::realsign_P) in
   let realsign_ind_G =
-    name_context env ((LocalAssum (Name varH,applied_ind_G))::
+    name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind_G))::
                       lift_rel_context (nrealargs+3) realsign) in
   let applied_sym_C n =
      mkApp(sym,
@@ -400,8 +409,9 @@ let build_l2r_rew_scheme dep env ind kind =
   let s, ctx' = UnivGen.fresh_sort_in_family kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
-  let ci = make_case_info (Global.env()) ind RegularStyle in
-  let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in
+  let rci = Sorts.Relevant in (* TODO relevance *)
+  let ci = make_case_info (Global.env()) ind rci RegularStyle in
+  let cieq = make_case_info (Global.env()) (fst (destInd eq)) rci RegularStyle in
   let applied_PC =
     mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect mkRel 1 realsign)
            (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
@@ -429,14 +439,14 @@ let build_l2r_rew_scheme dep env ind kind =
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign
-  (mkNamedLambda varP
+  (mkNamedLambda (make_annot varP indr)
     (my_it_mkProd_or_LetIn (if dep then realsign_ind_P else realsign_P) s)
-  (mkNamedLambda varHC applied_PC
-  (mkNamedLambda varH (lift 2 applied_ind)
+  (mkNamedLambda (make_annot varHC indr) applied_PC
+  (mkNamedLambda (make_annot varH indr) (lift 2 applied_ind)
   (if dep then (* we need a coercion *)
      mkCase (cieq,
-       mkLambda (Name varH,lift 3 applied_ind,
-         mkLambda (Anonymous,
+       mkLambda (make_annot (Name varH) indr,lift 3 applied_ind,
+         mkLambda (make_annot Anonymous indr,
                    mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
                    applied_PR)),
        mkApp (sym_involutive,
@@ -481,7 +491,9 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     mkApp (mkConstructUi(indu,1),
       Array.concat [Context.Rel.to_extended_vect mkRel n paramsctxt1;
                     rel_vect p nrealargs]) in
-  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let inds = snd (mind_arity mip) in
+  let indr = Sorts.relevance_of_sort_family inds in
+  let varH = fresh env (default_id_of_sort inds) in
   let varHC = fresh env (Id.of_string "HC") in
   let varP = fresh env (Id.of_string "P") in
   let applied_ind = build_dependent_inductive indu specif in
@@ -497,13 +509,14 @@ let build_l2r_forward_rew_scheme dep env ind kind =
         rel_vect (2*nrealargs+1) nrealargs]) in
   let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
   let realsign_ind =
-    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
+    name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
   let realsign_ind_P n aP =
-    name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in
+    name_context env ((LocalAssum (make_annot (Name varH) indr,aP))::realsign_P n) in
   let s, ctx' = UnivGen.fresh_sort_in_family kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
-  let ci = make_case_info (Global.env()) ind RegularStyle in
+  let rci = Sorts.Relevant in
+  let ci = make_case_info (Global.env()) ind rci RegularStyle in
   let applied_PC =
     mkApp (mkVar varP,Array.append
            (rel_vect (nrealargs*2+3) nrealargs)
@@ -519,19 +532,19 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign
-  (mkNamedLambda varH applied_ind
+  (mkNamedLambda (make_annot varH indr) applied_ind
   (mkCase (ci,
      my_it_mkLambda_or_LetIn_name
        (lift_rel_context (nrealargs+1) realsign_ind)
-       (mkNamedProd varP
+       (mkNamedProd (make_annot varP indr)
          (my_it_mkProd_or_LetIn
 	   (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s)
-       (mkNamedProd varHC applied_PC applied_PG)),
+       (mkNamedProd (make_annot varHC indr) applied_PC applied_PG)),
      (mkVar varH),
-     [|mkNamedLambda varP
+     [|mkNamedLambda (make_annot varP indr)
         (my_it_mkProd_or_LetIn
 	  (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
-      (mkNamedLambda varHC applied_PC'
+      (mkNamedLambda (make_annot varHC indr) applied_PC'
 	(mkVar varHC))|])))))
   in c, UState.of_context_set ctx
 
@@ -572,16 +585,19 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let cstr n =
     mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect mkRel n mib.mind_params_ctxt) in
   let constrargs_cstr = constrargs@[cstr 0] in
-  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let inds = snd (mind_arity mip) in
+  let indr = Sorts.relevance_of_sort_family inds in
+  let varH = fresh env (default_id_of_sort inds) in
   let varHC = fresh env (Id.of_string "HC") in
   let varP = fresh env (Id.of_string "P") in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
-    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
+    name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
   let s, ctx' = UnivGen.fresh_sort_in_family kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
-  let ci = make_case_info (Global.env()) ind RegularStyle in
+  let rci = Sorts.Relevant in (* TODO relevance *)
+  let ci = make_case_info (Global.env()) ind rci RegularStyle in
   let applied_PC =
     applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
   let applied_PG =
@@ -591,18 +607,18 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
-  (mkNamedLambda varP
+  (mkNamedLambda (make_annot varP indr)
     (my_it_mkProd_or_LetIn (lift_rel_context (nrealargs+1)
                              (if dep then realsign_ind else realsign)) s)
-  (mkNamedLambda varHC (lift 1 applied_PG)
+  (mkNamedLambda (make_annot varHC indr) (lift 1 applied_PG)
   (mkApp
     (mkCase (ci,
        my_it_mkLambda_or_LetIn_name
          (lift_rel_context (nrealargs+3) realsign_ind)
-         (mkArrow applied_PG (lift (2*nrealargs+5) applied_PC)),
+         (mkArrow applied_PG indr (lift (2*nrealargs+5) applied_PC)),
        mkRel 3 (* varH *),
        [|mkLambda
-          (Name varHC,
+          (make_annot (Name varHC) indr,
 	   lift (nrealargs+3) applied_PC,
 	   mkRel 1)|]),
     [|mkVar varHC|]))))))
@@ -775,7 +791,10 @@ let build_congr env (eq,refl,ctx) ind =
   if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let env_with_arity = push_rel_context arityctxt env in
-  let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
+  let ty, tyr =
+    let decl = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
+    RelDecl.get_type decl, RelDecl.get_relevance decl
+  in
   let constrsign,ccl = mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
@@ -784,15 +803,16 @@ let build_congr env (eq,refl,ctx) ind =
   let varB = fresh env (Id.of_string "B") in
   let varH = fresh env (Id.of_string "H") in
   let varf = fresh env (Id.of_string "f") in
-  let ci = make_case_info (Global.env()) ind RegularStyle in
+  let rci = Sorts.Relevant in (* TODO relevance *)
+  let ci = make_case_info (Global.env()) ind rci RegularStyle in
   let uni, ctx = Univ.extend_in_context_set (UnivGen.new_global_univ ()) ctx in
   let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
   let c = 
   my_it_mkLambda_or_LetIn paramsctxt
-     (mkNamedLambda varB (mkSort (Type uni))
-     (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB))
+     (mkNamedLambda (make_annot varB Sorts.Relevant) (mkType uni)
+     (mkNamedLambda (make_annot varf Sorts.Relevant) (mkArrow (lift 1 ty) tyr (mkVar varB))
      (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign)
-     (mkNamedLambda varH
+     (mkNamedLambda (make_annot varH Sorts.Relevant)
         (applist
            (mkIndU indu,
 	    Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @
@@ -801,7 +821,7 @@ let build_congr env (eq,refl,ctx) ind =
        my_it_mkLambda_or_LetIn_name
 	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
          (mkLambda
-           (Anonymous,
+           (make_annot Anonymous Sorts.Relevant,
             applist
              (mkIndU indu,
 	        Context.Rel.to_extended_list mkRel (2*mip.mind_nrealdecls+3)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4a1bb37fa4..88ce9868af 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -16,6 +16,7 @@ open Names
 open Nameops
 open Term
 open Constr
+open Context
 open Termops
 open EConstr
 open Vars
@@ -887,7 +888,8 @@ let descend_then env sigma head dirn =
       let brl =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
-      let ci = make_case_info env ind RegularStyle in
+      let rci = Sorts.Relevant in (* TODO relevance *)
+      let ci = make_case_info env ind rci RegularStyle in
       Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
 
 (* Now we need to construct the discriminator, given a discriminable
@@ -932,7 +934,8 @@ let build_selector env sigma dirn c ind special default =
     it_mkLambda_or_LetIn endpt args in
   let brl =
     List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
-  let ci = make_case_info env ind RegularStyle in
+  let rci = Sorts.Relevant in (* TODO relevance *)
+  let ci = make_case_info env ind rci RegularStyle in
   let ans = Inductiveops.make_case_or_project env sigma indf ci p c (Array.of_list brl) in
   ans
 
@@ -997,7 +1000,7 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq =
   Proofview.tclEFFECTS eff <*>
     pf_constr_of_global eq_elim >>= fun eq_elim ->
     Proofview.tclUNIT
-       (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term)
+       (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]), absurd_term)
 
 
 let eq_baseid = Id.of_string "e"
@@ -1015,7 +1018,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   build_coq_True () >>= fun true_0 ->
   build_coq_False () >>= fun false_0 ->
   let e = next_ident_away eq_baseid (vars_of_env env) in
-  let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
+  let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e Sorts.Relevant,t)) env in
   let discriminator =
     try
       Proofview.tclUNIT
@@ -1025,7 +1028,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   in
     discriminator >>= fun discriminator ->
     discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) ->
-    let pf_ty = mkArrow eqn absurd_term in
+    let pf_ty = mkArrow eqn Sorts.Relevant absurd_term in
     let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
     let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
     tclTHENS (assert_after Anonymous absurd_term)
@@ -1114,7 +1117,7 @@ let make_tuple env sigma (rterm,rty) lind =
   assert (not (noccurn sigma lind rty));
   let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
   let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
-  let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
+  let na = Context.Rel.Declaration.get_annot (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
   (* Now [lind] is [mkRel 1] and we abstract on (na:a) *)
@@ -1374,13 +1377,13 @@ let simplify_args env sigma t =
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   let e = next_ident_away eq_baseid (vars_of_env env) in
-  let e_env = push_named (LocalAssum (e,t)) env in
+  let e_env = push_named (LocalAssum (make_annot e Sorts.Relevant,t)) env in
   let evdref = ref sigma in
   let filter (cpath, t1', t2') =
     try
       (* arbitrarily take t1' as the injector default value *)
       let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in
-      let injfun = mkNamedLambda e t injbody in
+      let injfun = mkNamedLambda (make_annot e Sorts.Relevant) t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
       let sigma, pf_typ = Typing.type_of env sigma pf in
@@ -1565,9 +1568,9 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env sigma (t,subst_term sigma e body)) e1_list b in
+      (fun (e,t) body -> lambda_create env sigma (Sorts.Relevant,t,subst_term sigma e body)) e1_list b in
   let pred_body = beta_applist sigma (abst_B,proj_list) in
-  let body = mkApp (lambda_create env sigma (typ,pred_body),[|dep_pair1|]) in
+  let body = mkApp (lambda_create env sigma (Sorts.Relevant,typ,pred_body),[|dep_pair1|]) in
   let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota env sigma expected_goal in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c1f6365f5d..a04a9f9db9 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -13,6 +13,7 @@ open Util
 open CErrors
 open Names
 open Constr
+open Context
 open Evd
 open EConstr
 open Vars
@@ -1275,7 +1276,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in
       vars := Id.Set.add id !vars;
       subst := (evar,mkVar id)::!subst;
-      mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in
+      mkNamedLambda (make_annot id Sorts.Relevant) t (iter (replace_term sigma evar (mkVar id) c)) in
   let c' = iter c in
     let env = Global.env () in
     let empty_sigma = Evd.from_env env in
@@ -1305,7 +1306,7 @@ let project_hint ~poly pri l2r r =
   let sigma, p = Evd.fresh_global env sigma p in
   let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
   let c = it_mkLambda_or_LetIn
-    (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
+    (mkApp (p,[|mkArrow a Sorts.Relevant (lift 1 b);mkArrow b Sorts.Relevant (lift 1 a);c|])) sign in
   let id =
     Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
   in
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 395b4928ce..08131f6309 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -182,10 +182,10 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
       let car = constructors_nrealargs ind in
       let (mib,mip) = Global.lookup_inductive ind in
       if Array.for_all (fun ar -> Int.equal ar 1) car
-	&& not (mis_is_recursive (ind,mib,mip))
-        && (Int.equal mip.mind_nrealargs 0)
+      && not (mis_is_recursive (ind,mib,mip))
+      && (Int.equal mip.mind_nrealargs 0)
       then
-	if strict then
+        if strict then
           if test_strict_disjunction (mib, mip) then
 	    Some (hdapp,args)
 	  else
@@ -196,7 +196,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
             pi2 (destProd sigma (prod_applist sigma ar args))
           in
           let cargs = Array.map map mip.mind_nf_lc in
-	  Some (hdapp,Array.to_list cargs)
+          Some (hdapp,Array.to_list cargs)
       else
 	None
   | _ -> None in
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index f04cda1232..741f6713e3 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -86,7 +86,7 @@ val is_equality_type       : testing_function
 val match_with_nottype     : Environ.env -> (constr * constr) matching_function
 val is_nottype             : Environ.env -> testing_function
 
-val match_with_forall_term    : (Name.t * constr * constr) matching_function
+val match_with_forall_term    : (Name.t Context.binder_annot * constr * constr) matching_function
 val is_forall_term            : testing_function
 
 val match_with_imp_term    : (constr * constr) matching_function
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 2ae37ab471..776148d4cf 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -15,6 +15,7 @@ open Names
 open Term
 open Termops
 open Constr
+open Context
 open EConstr
 open Vars
 open Namegen
@@ -131,7 +132,7 @@ let make_inv_predicate env evd indf realargs id status concl =
         let eq_term = eqdata.Coqlib.eq in
         let eq = evd_comb1 (Evd.fresh_global env) evd eq_term in
         let eqn = applist (eq,[eqnty;lhs;rhs]) in
-        let eqns = (Anonymous, lift n eqn) :: eqns in
+        let eqns = (make_annot Anonymous Sorts.Relevant, lift n eqn) :: eqns in
         let refl_term = eqdata.Coqlib.refl in
         let refl_term = evd_comb1 (Evd.fresh_global env) evd refl_term in
         let refl = mkApp (refl_term, [|eqnty; rhs|]) in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 335f3c74ff..4aa4d13e1e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -15,6 +15,7 @@ open Names
 open Termops
 open Environ
 open Constr
+open Context
 open EConstr
 open Vars
 open Namegen
@@ -120,13 +121,13 @@ let max_prefix_sign lid sign =
 let rec add_prods_sign env sigma t =
   match EConstr.kind sigma (whd_all env sigma t) with
     | Prod (na,c1,b) ->
-	let id = id_of_name_using_hdchar env sigma t na in
+        let id = id_of_name_using_hdchar env sigma t na.binder_name in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b'
+        add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b'
     | LetIn (na,c1,t1,b) ->
-	let id = id_of_name_using_hdchar env sigma t na in
+        let id = id_of_name_using_hdchar env sigma t na.binder_name in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b'
+        add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates whether the inversion lemma is dependent or not.
@@ -149,9 +150,10 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
   let pty,goal =
     if dep_option  then
       let pty = make_arity env sigma true indf sort in
+      let r = relevance_of_inductive_type env ind in
       let goal =
 	mkProd
-	  (Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
+          (make_annot Anonymous r, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
       in
       pty,goal
     else
@@ -169,11 +171,11 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
           env ~init:([],[])
       in
       let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
-      let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
+      let goal = mkArrow i Sorts.Relevant (applist(mkVar p, List.rev revargs)) in
       (pty,goal)
   in
   let npty = nf_all env sigma pty in
-  let extenv = push_named (LocalAssum (p,npty)) env in
+  let extenv = push_named (LocalAssum (make_annot p Sorts.Relevant,npty)) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
@@ -225,7 +227,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
 	let h = next_ident_away (Id.of_string "H") !avoid in
 	let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
 	avoid := Id.Set.add h !avoid;
-	ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign;
+        ownSign := Context.Named.add (LocalAssum (make_annot h Sorts.Relevant,ty)) !ownSign;
 	applist (mkVar h, inst)
     | _ -> EConstr.map sigma fill_holes c
   in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 415225454a..b8308dc49b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -14,6 +14,7 @@ open Util
 open Names
 open Nameops
 open Constr
+open Context
 open Termops
 open Environ
 open EConstr
@@ -137,8 +138,8 @@ let introduction id =
     in
     let open Context.Named.Declaration in
     match EConstr.kind sigma concl with
-    | Prod (_, t, b) -> unsafe_intro env (LocalAssum (id, t)) b
-    | LetIn (_, c, t, b) -> unsafe_intro env (LocalDef (id, c, t)) b
+    | Prod (id0, t, b) -> unsafe_intro env (LocalAssum ({id0 with binder_name=id}, t)) b
+    | LetIn (id0, c, t, b) -> unsafe_intro env (LocalDef ({id0 with binder_name=id}, c, t)) b
     | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
   end
 
@@ -366,8 +367,8 @@ let default_id env sigma decl =
   match decl with
   | LocalAssum (name,t) ->
       let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in
-      id_of_name_with_default dft name
-  | LocalDef (name,b,_) -> id_of_name_using_hdchar env sigma b name
+      id_of_name_with_default dft name.binder_name
+  | LocalDef (name,b,_) -> id_of_name_using_hdchar env sigma b name.binder_name
 
 (* Non primitive introduction tactics are treated by intro_then_gen
    There is possibly renaming, with possibly names to avoid and
@@ -437,16 +438,17 @@ let internal_cut_gen ?(check=true) dir replace id t =
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
     let sign = named_context_val env in
+    let r = Retyping.relevance_of_type env sigma t in
     let sign',t,concl,sigma =
       if replace then
         let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
         let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
-        let sign' = insert_decl_in_named_context env sigma (LocalAssum (id,t)) nexthyp sign' in
+        let sign' = insert_decl_in_named_context env sigma (LocalAssum (make_annot id r,t)) nexthyp sign' in
         sign',t,concl,sigma
       else
         (if check && mem_named_context_val id sign then
 	   user_err (str "Variable " ++ Id.print id ++ str " is already declared.");
-         push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in
+         push_named_context_val (LocalAssum (make_annot id r,t)) sign,t,concl,sigma) in
     let nf_t = nf_betaiota env sigma t in
     Proofview.tclTHEN
       (Proofview.Unsafe.tclEVARS sigma)
@@ -460,7 +462,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
             let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
             let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
             (sigma,ev,ev') in
-        let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in
+        let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in
         (sigma, term)
       end)
   end
@@ -471,7 +473,7 @@ let internal_cut_rev ?(check=true) = internal_cut_gen ~check false
 let assert_before_then_gen b naming t tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter begin fun gl ->
-    let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
+    let id = find_name b (LocalAssum (make_annot Anonymous Sorts.Relevant,t)) naming gl in
     Tacticals.New.tclTHENLAST
       (internal_cut b id t)
       (tac id)
@@ -486,7 +488,7 @@ let assert_before_replacing id = assert_before_gen true (NamingMustBe (CAst.make
 let assert_after_then_gen b naming t tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter begin fun gl ->
-    let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
+    let id = find_name b (LocalAssum (make_annot Anonymous Sorts.Relevant,t)) naming gl in
     Tacticals.New.tclTHENFIRST
       (internal_cut_rev b id t)
       (tac id)
@@ -542,7 +544,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
     if mem_named_context_val f sign then
       user_err ~hdr:"Logic.prim_refiner"
         (str "Name " ++ Id.print f ++ str " already used in the environment");
-    mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
+    mk_sign (push_named_context_val (LocalAssum (make_annot f Sorts.Relevant, ar)) sign) oth
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
   Refine.refine ~typecheck:false begin fun sigma ->
@@ -550,7 +552,8 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
     let ids = List.map pi1 all in
     let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
     let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
-    let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+    (* TODO relevance *)
+    let funnames = Array.of_list (List.map (fun i -> make_annot (Name i) Sorts.Relevant) ids) in
     let typarray = Array.of_list (List.map pi3 all) in
     let bodies = Array.of_list evs in
     let oterm = mkFix ((indxs,0),(funnames,typarray,bodies)) in
@@ -586,14 +589,15 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl ->
     let open Context.Named.Declaration in
     if mem_named_context_val f sign then
       error "Name already used in the environment.";
-    mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
+    mk_sign (push_named_context_val (LocalAssum (make_annot f Sorts.Relevant, ar)) sign) oth
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
   Refine.refine ~typecheck:false begin fun sigma ->
     let (ids, types) = List.split all in
     let (sigma, evs) = mk_holes nenv sigma types in
     let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
-    let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+    (* TODO relevance *)
+    let funnames = Array.of_list (List.map (fun i -> make_annot (Name i) Sorts.Relevant) ids) in
     let typarray = Array.of_list types in
     let bodies = Array.of_list evs in
     let oterm = mkCoFix (0, (funnames, typarray, bodies)) in
@@ -616,7 +620,7 @@ let pf_reduce_decl redfun where decl gl =
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	user_err  (Id.print id ++ str " has no value.");
+        user_err  (Id.print id.binder_name ++ str " has no value.");
       LocalAssum (id,redfun' ty)
   | LocalDef (id,b,ty) ->
       let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -717,7 +721,7 @@ let pf_e_reduce_decl redfun where decl gl =
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	user_err  (Id.print id ++ str " has no value.");
+        user_err  (Id.print id.binder_name ++ str " has no value.");
     let (sigma, ty') = redfun sigma ty in
     (sigma, LocalAssum (id, ty'))
   | LocalDef (id,b,ty) ->
@@ -760,7 +764,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	user_err  (Id.print id ++ str " has no value.");
+        user_err  (Id.print id.binder_name ++ str " has no value.");
     let (sigma, ty') = redfun false env sigma ty in
     (sigma, LocalAssum (id, ty'))
   | LocalDef (id,b,ty) ->
@@ -947,7 +951,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
         let name = find_name false (LocalDef (name,b,t)) name_flag gl in
 	build_intro_tac name move_flag tac
     | Evar ev when force_flag ->
-        let sigma, t = Evardefine.define_evar_as_product sigma ev in
+        let sigma, t = Evardefine.define_evar_as_product env sigma ev in
         Tacticals.New.tclTHEN
           (Proofview.Unsafe.tclEVARS sigma)
           (intro_then_gen name_flag move_flag force_flag dep_flag tac)
@@ -1238,27 +1242,29 @@ let cut c =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
-    let is_sort =
+    let relevance =
       try
-        (* Backward compat: ensure that [c] is well-typed. *)
+        (* Backward compat: ensure that [c] is well-typed. Plus we
+           need to know the relevance *)
         let typ = Typing.unsafe_type_of env sigma c in
         let typ = whd_all env sigma typ in
         match EConstr.kind sigma typ with
-        | Sort _ -> true
-        | _ -> false
-      with e when Pretype_errors.precatchable_exception e -> false
+        | Sort s -> Some (Sorts.relevance_of_sort (ESorts.kind sigma s))
+        | _ -> None
+      with e when Pretype_errors.precatchable_exception e -> None
     in
-    if is_sort then
+    match relevance with
+    | Some r ->
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
       (* Backward compat: normalize [c]. *)
       let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
       Refine.refine ~typecheck:false begin fun h ->
-        let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
+        let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
         let (h, x) = Evarutil.new_evar env h c in
-        let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
+        let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
         (h, f)
       end
-    else
+    | None ->
       Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
   end
 
@@ -1823,7 +1829,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
   let sigma = Tacmach.New.project gl in
   let t' = Tacmach.New.pf_get_hyp_typ id gl in
   let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
-  let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
+  let targetid = find_name true (LocalAssum (make_annot Anonymous Sorts.Relevant,t')) naming gl in
   let rec aux idstoclear with_destruct c =
     Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -1890,7 +1896,7 @@ let cut_and_apply c =
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
         Refine.refine ~typecheck:false begin fun sigma ->
-          let typ = mkProd (Anonymous, c2, concl) in
+          let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in
           let (sigma, f) = Evarutil.new_evar env sigma typ in
           let (sigma, x) = Evarutil.new_evar env sigma c1 in
           (sigma, mkApp (f, [|mkApp (c, [|x|])|]))
@@ -2013,12 +2019,12 @@ let clear_body ids =
     let ctx = named_context env in
     let map = function
     | LocalAssum (id,t) as decl ->
-      let () = if List.mem_f Id.equal id ids then
-        user_err  (str "Hypothesis " ++ Id.print id ++ str " is not a local definition")
+      let () = if List.mem_f Id.equal id.binder_name ids then
+        user_err  (str "Hypothesis " ++ Id.print id.binder_name ++ str " is not a local definition")
       in
       decl
     | LocalDef (id,_,t) as decl ->
-      if List.mem_f Id.equal id ids then LocalAssum (id, t) else decl
+      if List.mem_f Id.equal id.binder_name ids then LocalAssum (id, t) else decl
     in
     let ctx = List.map map ctx in
     let base_env = reset_context env in
@@ -2624,7 +2630,8 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
           let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
           let eq = applist (eq,args) in
           let refl = applist (refl, [t;mkVar id]) in
-	  let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
+          let term = mkNamedLetIn (make_annot id Sorts.Relevant) c t
+              (mkLetIn (make_annot (Name heq) Sorts.Relevant, refl, eq, ccl)) in
 	  let sigma, _ = Typing.type_of env sigma term in
           let ans = term,
             Tacticals.New.tclTHENLIST
@@ -2634,7 +2641,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
           in
           (sigma, ans)
       | None ->
-          (sigma, (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()))
+          (sigma, (mkNamedLetIn (make_annot id Sorts.Relevant) c t ccl, Proofview.tclUNIT ()))
     in
       Tacticals.New.tclTHENLIST
       [ Proofview.Unsafe.tclEVARS sigma;
@@ -2669,8 +2676,9 @@ let mk_eq_name env id {CAst.loc;v=ido} =
 let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty =
   let open Context.Named.Declaration in
   let t = match ty with Some t -> t | _ -> typ_of env sigma c in
-  let decl = if dep then LocalDef (id,c,t)
-	     else LocalAssum (id,t)
+  let r = Retyping.relevance_of_type env sigma t in
+  let decl = if dep then LocalDef (make_annot id r,c,t)
+             else LocalAssum (make_annot id r,t)
   in
   match with_eq with
   | Some (lr,heq) ->
@@ -2680,13 +2688,14 @@ let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty =
       let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
-      let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
+      let newenv = insert_before [LocalAssum (make_annot heq Sorts.Relevant,eq); decl] lastlhyp env in
       let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
-      (sigma, mkNamedLetIn id c t (mkNamedLetIn heq refl eq x))
+      (sigma, mkNamedLetIn (make_annot id r) c t
+         (mkNamedLetIn (make_annot heq Sorts.Relevant) refl eq x))
   | None ->
       let newenv = insert_before [decl] lastlhyp env in
       let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
-      (sigma, mkNamedLetIn id c t x)
+      (sigma, mkNamedLetIn (make_annot id r) c t x)
 
 let pose_tac na c =
   Proofview.Goal.enter begin fun gl ->
@@ -2708,11 +2717,13 @@ let pose_tac na c =
     in
     Proofview.Unsafe.tclEVARS sigma <*>
     Refine.refine ~typecheck:false begin fun sigma ->
+      (* TODO relevance *)
+      let id = make_annot id Sorts.Relevant in
       let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in
       let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in
       let inst = Array.map_of_list (fun d -> mkVar (get_id d)) (named_context env) in
       let body = mkEvar (ev, Array.append [|mkRel 1|] inst) in
-      (sigma, mkLetIn (Name id, c, t, body))
+      (sigma, mkLetIn (map_annot Name.mk_name id, c, t, body))
     end
   end
 
@@ -2806,9 +2817,10 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
   let na = generalized_name env sigma c t ids cl' na in
+  let r = Retyping.relevance_of_type env sigma t in
   let decl = match b with
-    | None -> LocalAssum (na,t)
-    | Some b -> LocalDef (na,b,t)
+    | None -> LocalAssum (make_annot na r,t)
+    | Some b -> LocalDef (make_annot na r,b,t)
   in
   mkProd_or_LetIn decl cl', sigma'
 
@@ -2948,8 +2960,8 @@ let specialize (c,lbind) ipat =
       (* If the term is lambda then we put a letin to put avoid
          interaction between the term and the bindings. *)
       let c = match EConstr.kind sigma c with
-        | Lambda(_,_,_) ->
-          mkLetIn(Name.Anonymous, c, typ_of_c, (mkRel 1))
+        | Lambda _ ->
+          mkLetIn(make_annot Name.Anonymous Sorts.Relevant, c, typ_of_c, (mkRel 1))
         | _ -> c in
       let clause = make_clenv_binding env sigma (c,typ_of_c) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
@@ -2973,14 +2985,15 @@ let specialize (c,lbind) ipat =
           (* nme has not been resolved, let us re-abstract it. Same
              name but type updated by instanciation of other args. *)
           let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in
+          let r = Retyping.relevance_of_type env sigma new_typ_of_t in
           let liftedargs = List.map liftrel args in
           (* lifting rels in the accumulator args *)
           let sigma,hd' = rebuild_lambdas sigma lp' (liftedargs@[mkRel 1 ]) hd l' in
           (* replace meta variable by the abstracted variable *)
           let hd'' = subst_term sigma t hd' in
           (* lambda expansion *)
-          sigma,mkLambda (nme,new_typ_of_t,hd'')
-        | Context.Rel.Declaration.LocalAssum(_,_)::lp' , t::l' ->
+          sigma,mkLambda ({nme with binder_relevance=r},new_typ_of_t,hd'')
+        | Context.Rel.Declaration.LocalAssum _::lp' , t::l' ->
           let sigma,hd' = rebuild_lambdas sigma lp' (args@[t]) hd l' in
           sigma,hd'
         | _ ,_ -> assert false in
@@ -3631,15 +3644,18 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
       let homogeneous = Reductionops.is_conv env sigma ty typ in
       let sigma, (eq, refl) =
         mk_term_eq homogeneous (push_rel_context ctx env) sigma ty (mkRel 1) typ (mkVar id) in
-      sigma, mkProd (Anonymous, eq, lift 1 concl), [| refl |]
+      sigma, mkProd (make_annot Anonymous Sorts.Relevant, eq, lift 1 concl), [| refl |]
     else sigma, concl, [||]
   in
     (* Abstract by equalities *)
   let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
-  let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> LocalAssum (Anonymous, x)) eqs) in
+  let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq)
+      (List.map (fun x -> LocalAssum (make_annot Anonymous Sorts.Relevant, x)) eqs)
+  in
+  let r = Sorts.Relevant in (* TODO relevance *)
   let decl = match body with
-    | None -> LocalAssum (Name id, c)
-    | Some body -> LocalDef (Name id, body, c)
+    | None -> LocalAssum (make_annot (Name id) r, c)
+    | Some body -> LocalDef (make_annot (Name id) r, body, c)
   in
     (* Abstract by the "generalized" hypothesis. *)
   let genarg = mkProd_or_LetIn decl abseqs in
@@ -3714,10 +3730,10 @@ let abstract_args gl generalize_vars dep id defined f args =
        eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
     *)
   let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg =
-    let name, ty, arity =
+    let name, ty_relevance, ty, arity =
       let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
       let decl = List.hd rel in
-      RelDecl.get_name decl, RelDecl.get_type decl, c
+      RelDecl.get_name decl, RelDecl.get_relevance decl, RelDecl.get_type decl, c
     in
     let argty = Tacmach.New.pf_unsafe_type_of gl arg in
     let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
@@ -3731,7 +3747,7 @@ let abstract_args gl generalize_vars dep id defined f args =
       	  Id.Set.add id nongenvars, Id.Set.remove id vars, env)
       | _ ->
 	  let name = get_id name in
-	  let decl = LocalAssum (Name name, ty) in
+          let decl = LocalAssum (make_annot (Name name) ty_relevance, ty) in
 	  let ctx = decl :: ctx in
 	  let c' = mkApp (lift 1 c, [|mkRel 1|]) in
 	  let args = arg :: args in
@@ -3869,7 +3885,7 @@ let specialize_eqs id =
 	    else
               let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in
               evars := sigma;
-		aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
+                aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
     | t -> acc, in_eqs, ctx, ty
   in
   let acc, worked, ctx, ty = aux false [] (mkVar id) ty in
@@ -3917,7 +3933,7 @@ let decompose_paramspred_branch_args sigma elimt =
       | Prod(nme,tpe,elimt') ->
 	  let hd_tpe,_ = decompose_app sigma (snd (decompose_prod_assum sigma tpe)) in
 	  if not (occur_rel sigma 1 elimt') && isRel sigma hd_tpe
-	  then cut_noccur elimt' (LocalAssum (nme,tpe)::acc2)
+          then cut_noccur elimt' (LocalAssum (nme,tpe)::acc2)
 	  else let acc3,ccl = decompose_prod_assum sigma elimt in acc2 , acc3 , ccl
       | App(_, _) | Rel _ -> acc2 , [] , elimt
       | _ -> error_ind_scheme "" in
@@ -3999,8 +4015,8 @@ let compute_elim_sig sigma ?elimc elimt =
     (* 3- Look at last arg: is it the indarg? *)
     ignore (
       match List.hd args_indargs with
-	| LocalDef (hiname,_,hi) -> error_ind_scheme ""
-	| LocalAssum (hiname,hi) ->
+        | LocalDef (hiname,_,hi) -> error_ind_scheme ""
+        | LocalAssum (hiname,hi) ->
 	    let hi_ind, hi_args = decompose_app sigma hi in
 	    let hi_is_ind = (* hi est d'un type globalisable *)
 	      match EConstr.kind sigma hi_ind with
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e8a66f1889..2831aec9f6 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -316,7 +316,7 @@ struct
       Term(DCoFix(i,Array.map pat_of_constr ta,Array.map pat_of_constr ca))
     | Cast (c,_,_)   -> pat_of_constr c
     | Lambda (_,t,c) -> Term(DLambda (pat_of_constr t, pat_of_constr c))
-    | (Prod (_,_,_) | LetIn(_,_,_,_))   ->
+    | (Prod _ | LetIn _)   ->
       let (ctx,c) = ctx_of_constr (Term DNil) c in Term (DCtx (ctx,c))
     | App (f,ca)     ->
       Array.fold_left (fun c a -> Term (DApp (c,a)))