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

8 files changed, 89 insertions, 65 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 0961edb6cb..58daa7a7d4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -15,6 +15,7 @@ open Names
 open Evd
 open Term
 open Constr
+open Context
 open Termops
 open Printer
 open Locusops
@@ -429,15 +430,16 @@ let convert_concl t = Tactics.convert_concl t DEFAULTcast
 
 let rename_hd_prod orig_name_ref gl =
   match EConstr.kind (project gl) (pf_concl gl) with
-  | Prod(_,src,tgt) ->
-      Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl
+  | Prod(x,src,tgt) ->
+    let x = {x with binder_name = !orig_name_ref} in
+      Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (x,src,tgt))) gl
   | _ -> CErrors.anomaly (str "gentac creates no product")
 
 (* Reduction that preserves the Prod/Let spine of the "in" tactical. *)
 
 let inc_safe n = if n = 0 then n else n + 1
 let rec safe_depth s c = match EConstr.kind s c with
-| LetIn (Name x, _, _, c') when is_discharged_id x -> safe_depth s c' + 1
+| LetIn ({binder_name=Name x}, _, _, c') when is_discharged_id x -> safe_depth s c' + 1
 | LetIn (_, _, _, c') | Prod (_, _, c') -> inc_safe (safe_depth s c')
 | _ -> 0 
 
@@ -529,7 +531,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) =
     let concl = EConstr.Unsafe.to_constr evi.evar_concl in
     let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in
     let abs_dc c = function
-    | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c)
+    | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t x.binder_relevance c)
     | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in
     let t = Context.Named.fold_inside abs_dc ~init:concl dc in
     nf_evar sigma t in
@@ -552,7 +554,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) =
   | _ -> Constr.map_with_binders ((+) 1) get i c in
   let rec loop c i = function
   | (_, (n, t)) :: evl ->
-    loop (mkLambda (mk_evar_name n, get (i - 1) t, c)) (i - 1) evl
+    loop (mkLambda (make_annot (mk_evar_name n) Sorts.Relevant, get (i - 1) t, c)) (i - 1) evl
   | [] -> c in
   List.length evlist, EConstr.of_constr (loop (get 1 c0) 1 evlist), List.map fst evlist, ucst
 
@@ -590,7 +592,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
     let concl = EConstr.Unsafe.to_constr evi.evar_concl in
     let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in
     let abs_dc c = function
-    | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c)
+    | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t x.binder_relevance c)
     | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in
     let t = Context.Named.fold_inside abs_dc ~init:concl dc in
     nf_evar sigma0 (nf_evar sigma t) in
@@ -646,7 +648,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   | (_, (n, t, _)) :: evl ->
     let t = get evlist (i - 1) t in
     let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in 
-    loopP evlist (mkProd (n, t, c)) (i - 1) evl
+    loopP evlist (mkProd (make_annot n Sorts.Relevant, t, c)) (i - 1) evl
   | [] -> c in
   let rec loop c i = function
   | (_, (n, t, _)) :: evl ->
@@ -658,7 +660,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
       List.map (fun (k,_) -> mkRel (fst (lookup k i evlist))) 
         (List.rev t_evplist) in
     let c = if extra_args = [] then c else app extra_args 1 c in
-    loop (mkLambda (mk_evar_name n, t, c)) (i - 1) evl
+    loop (mkLambda (make_annot (mk_evar_name n) Sorts.Relevant, t, c)) (i - 1) evl
   | [] -> c in
   let res = loop (get evlist 1 c0) 1 evlist in
   pp(lazy(str"res= " ++ pr_constr res));
@@ -679,6 +681,9 @@ let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t)
 let pfe_type_of gl t =
   let sigma, ty = pf_type_of gl t in
   re_sig (sig_it gl) sigma, ty
+let pfe_type_relevance_of gl t =
+  let gl, ty = pfe_type_of gl t in
+  gl, ty, pf_apply Retyping.relevance_of_term gl t
 let pf_type_of gl t =
   let sigma, ty = pf_type_of gl (EConstr.of_constr t) in
   re_sig (sig_it gl)  sigma, EConstr.Unsafe.to_constr ty
@@ -710,13 +715,13 @@ let pf_abs_cterm gl n c0 =
   | _ -> [], strip i c in
   let rec strip_evars i c = match Constr.kind c with
     | Lambda (x, t1, c1) when i < n ->
-      let na = nb_evar_deps x in
+      let na = nb_evar_deps x.binder_name in
       let dl, t2 = strip_ndeps (i + na) i t1 in
       let na' = List.length dl in
       eva.(i) <- Array.of_list (na - na' :: dl);
       let x' =
         if na' = 0 then Name (pf_type_id gl (EConstr.of_constr t2)) else mk_evar_name na' in
-      mkLambda (x', t2, strip_evars (i + 1) c1)
+      mkLambda ({x with binder_name=x'}, t2, strip_evars (i + 1) c1)
 (*      if noccurn 1 c2 then lift (-1) c2 else
       mkLambda (Name (pf_type_id gl t2), t2, c2) *)
     | _ -> strip i c in
@@ -739,9 +744,9 @@ let rec constr_name sigma c = match EConstr.kind sigma c with
   | _ -> Anonymous
 
 let pf_mkprod gl c ?(name=constr_name (project gl) c) cl =
-  let gl, t = pfe_type_of gl c in
-  if name <> Anonymous || EConstr.Vars.noccurn (project gl) 1 cl then gl, EConstr.mkProd (name, t, cl) else
-  gl, EConstr.mkProd (Name (pf_type_id gl t), t, cl)
+  let gl, t, r = pfe_type_relevance_of gl c in
+  if name <> Anonymous || EConstr.Vars.noccurn (project gl) 1 cl then gl, EConstr.mkProd (make_annot name r, t, cl) else
+  gl, EConstr.mkProd (make_annot (Name (pf_type_id gl t)) r, t, cl)
 
 let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project gl) c cl)
 
@@ -783,13 +788,17 @@ let mkRefl t c gl =
 
 let discharge_hyp (id', (id, mode)) gl =
   let cl' = Vars.subst_var id (pf_concl gl) in
-  match pf_get_hyp gl id, mode with
-  | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" ->
-     Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl')))
+  let decl = pf_get_hyp gl id in
+  match decl, mode with
+  | NamedDecl.LocalAssum _, _ | NamedDecl.LocalDef _, "(" ->
+    let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in
+    Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true
+                               (EConstr.of_constr (mkProd (id', NamedDecl.get_type decl, cl')))
        [EConstr.of_constr (mkVar id)]) gl
   | NamedDecl.LocalDef (_, v, t), _ ->
+    let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in
      Proofview.V82.of_tactic
-       (convert_concl (EConstr.of_constr (mkLetIn (Name id', v, t, cl')))) gl
+       (convert_concl (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl
 
 (* wildcard names *)
 let clear_wilds wilds gl =
@@ -983,7 +992,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
       let rec loop sigma bo args = function (* saturate with metas *)
         | 0 -> EConstr.mkApp (t, Array.of_list (List.rev args)), re_sig si sigma 
         | n -> match EConstr.kind sigma bo with
-          | Lambda (_, ty, bo) -> 
+          | Lambda (_, ty, bo) ->
               if not (EConstr.Vars.closed0 sigma ty) then
                 raise dependent_apply_error;
               let m = Evarutil.new_meta () in
@@ -1019,7 +1028,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;;
 let rec fst_prod red tac = Proofview.Goal.enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
   match EConstr.kind (Proofview.Goal.sigma gl) concl with
-  | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id
+  | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id.binder_name
   | _ -> if red then Tacticals.New.tclZEROMSG (str"No product even after head-reduction.")
          else Tacticals.New.tclTHEN Tactics.hnf_in_concl (fst_prod true tac)
 end
@@ -1122,14 +1131,14 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
 	errorstrm (str "@ can be used with variables only")
       else match Tacmach.pf_get_hyp gl (EConstr.destVar sigma c) with
       | NamedDecl.LocalAssum _ -> errorstrm (str "@ can be used with let-ins only")
-      | NamedDecl.LocalDef (name, b, ty) -> true, pat, EConstr.mkLetIn (Name name,b,ty,cl),c,clr,ucst,gl
+      | NamedDecl.LocalDef (name, b, ty) -> true, pat, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl),c,clr,ucst,gl
     else let gl, ccl =  pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl
   else if to_ind && occ = None then
     let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in
     let ucst = UState.union ucst ucst' in
     if nv = 0 then anomaly "occur_existential but no evars" else
-    let gl, pty = pfe_type_of gl p in
-    false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl
+    let gl, pty, rp = pfe_type_relevance_of gl p in
+    false, pat, EConstr.mkProd (make_annot (constr_name (project gl) c) rp, pty, Tacmach.pf_concl gl), p, clr,ucst,gl
   else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match")
 
 let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs)
@@ -1235,7 +1244,10 @@ let abs_wgen keep_let f gen (gl,args,c) =
                      (EConstr.Vars.subst_var x c)
   | _, Some ((x, _), None) ->
      let x = hoi_id x in
-     gl, EConstr.mkVar x :: args, EConstr.mkProd (Name (f x),Tacmach.pf_get_hyp_typ gl x, EConstr.Vars.subst_var x c)
+     let hyp = Tacmach.pf_get_hyp gl x in
+     let x' = make_annot (Name (f x)) (NamedDecl.get_relevance hyp) in
+     let prod = EConstr.mkProd (x', NamedDecl.get_type hyp, EConstr.Vars.subst_var x c) in
+     gl, EConstr.mkVar x :: args, prod
   | _, Some ((x, "@"), Some p) -> 
      let x = hoi_id x in
      let cp = interp_cpattern gl p None in
@@ -1246,8 +1258,8 @@ let abs_wgen keep_let f gen (gl,args,c) =
      let t = EConstr.of_constr t in
      evar_closed t p;
      let ut = red_product_skip_id env sigma t in
-     let gl, ty = pfe_type_of gl t in
-     pf_merge_uc ucst gl, args, EConstr.mkLetIn(Name (f x), ut, ty, c)
+     let gl, ty, r = pfe_type_relevance_of gl t in
+     pf_merge_uc ucst gl, args, EConstr.mkLetIn(make_annot (Name (f x)) r, ut, ty, c)
   | _, Some ((x, _), Some p) ->
      let x = hoi_id x in
      let cp = interp_cpattern gl p None in
@@ -1257,8 +1269,8 @@ let abs_wgen keep_let f gen (gl,args,c) =
      let c = EConstr.of_constr c in
      let t = EConstr.of_constr t in
      evar_closed t p;
-     let gl, ty = pfe_type_of gl t in
-     pf_merge_uc ucst gl, t :: args, EConstr.mkProd(Name (f x), ty, c)
+     let gl, ty, r = pfe_type_relevance_of gl t in
+     pf_merge_uc ucst gl, t :: args, EConstr.mkProd(make_annot (Name (f x)) r, ty, c)
   | _ -> gl, args, c
 
 let clr_of_wgen gen clrs = match gen with
@@ -1321,8 +1333,8 @@ let unsafe_intro env decl b =
   end
 
 let set_decl_id id = let open Context in function
-  | Rel.Declaration.LocalAssum(name,ty) -> Named.Declaration.LocalAssum(id,ty)
-  | Rel.Declaration.LocalDef(name,ty,t) -> Named.Declaration.LocalDef(id,ty,t)
+  | Rel.Declaration.LocalAssum(name,ty) -> Named.Declaration.LocalAssum({name with binder_name=id},ty)
+  | Rel.Declaration.LocalDef(name,ty,t) -> Named.Declaration.LocalDef({name with binder_name=id},ty,t)
 
 let rec decompose_assum env sigma orig_goal =
   let open Context in
@@ -1400,8 +1412,8 @@ let tclRENAME_HD_PROD name = Goal.enter begin fun gl ->
   let concl = Goal.concl gl in
   let sigma = Goal.sigma gl in
   match EConstr.kind sigma concl with
-  | Prod(_,src,tgt) ->
-      convert_concl_no_check EConstr.(mkProd (name,src,tgt))
+  | Prod(x,src,tgt) ->
+      convert_concl_no_check EConstr.(mkProd ({x with binder_name = name},src,tgt))
   | _ -> CErrors.anomaly (Pp.str "rename_hd_prod: no head product")
 end
 
@@ -1429,11 +1441,12 @@ let tacMKPROD c ?name cl =
   tacCONSTR_NAME ?name c >>= fun name ->
   Goal.enter_one ~__LOC__ begin fun g ->
     let sigma, env = Goal.sigma g, Goal.env g in
+    let r = Retyping.relevance_of_term env sigma c in
     if name <> Names.Name.Anonymous || EConstr.Vars.noccurn sigma  1 cl
-    then tclUNIT (EConstr.mkProd (name, t, cl))
+    then tclUNIT (EConstr.mkProd (make_annot name r, t, cl))
     else
       let name = Names.Id.of_string (Namegen.hdchar env sigma t) in
-      tclUNIT (EConstr.mkProd (Names.Name.Name name, t, cl))
+      tclUNIT (EConstr.mkProd (make_annot (Name.Name name) r, t, cl))
 end
 
 let tacINTERP_CPATTERN cp =
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index e642b5e788..9662daa7c7 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -155,7 +155,7 @@ val pf_e_type_of :
 val splay_open_constr : 
            Goal.goal Evd.sigma ->
            evar_map * EConstr.t ->
-           (Names.Name.t * EConstr.t) list * EConstr.t
+           (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
 val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool
 
 val mk_term : ssrtermkind -> constr_expr -> ssrterm
@@ -205,6 +205,9 @@ val pf_type_of :
 val pfe_type_of :
            Goal.goal Evd.sigma ->
            EConstr.t -> Goal.goal Evd.sigma * EConstr.types
+val pfe_type_relevance_of :
+           Goal.goal Evd.sigma ->
+           EConstr.t -> Goal.goal Evd.sigma * EConstr.types * Sorts.relevance
 val pf_abs_prod :
            Name.t ->
            Goal.goal Evd.sigma ->
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 7216849948..82a88678f0 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -15,6 +15,7 @@ open Names
 open Printer
 open Term
 open Constr
+open Context
 open Termops
 open Tactypes
 open Tacmach
@@ -364,14 +365,14 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
         let gl, eq = get_eq_type gl in
         let gen_eq_tac, gl =
           let refl = EConstr.mkApp (eq, [|t; c; c|]) in
-          let new_concl = EConstr.mkArrow refl (EConstr.Vars.lift 1 (pf_concl orig_gl)) in 
+          let new_concl = EConstr.mkArrow refl Sorts.Relevant (EConstr.Vars.lift 1 (pf_concl orig_gl)) in
           let new_concl = fire_subst gl new_concl in
           let erefl, gl = mkRefl t c gl in
           let erefl = fire_subst gl erefl in
           apply_type new_concl [erefl], gl in
         let rel = k + if c_is_head_p then 1 else 0 in
         let src, gl = mkProt EConstr.mkProp EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in
-        let concl = EConstr.mkArrow src (EConstr.Vars.lift 1 concl) in
+        let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in
         let clr = if deps <> [] then clr else [] in
         concl, gen_eq_tac, clr, gl
     | _ -> concl, Tacticals.tclIDTAC, clr, gl in
@@ -446,7 +447,7 @@ let injecteq_id = mk_internal_id "injection equation"
 let revtoptac n0 gl =
   let n = pf_nb_prod gl - n0 in
   let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in
-  let dc' = dc @ [Context.Rel.Declaration.LocalAssum(Name rev_id, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in
+  let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in
   let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in
   Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl
 
@@ -486,7 +487,7 @@ let perform_injection c gl =
     CErrors.user_err (Pp.str "can't decompose a quantified equality") else
   let cl = pf_concl gl in let n = List.length dc in
   let c_eq = mkEtaApp c n 2 in
-  let cl1 = EConstr.mkLambda EConstr.(Anonymous, mkArrow eqt cl, mkApp (mkRel 1, [|c_eq|])) in
+  let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in
   let id = injecteq_id in
   let id_with_ebind = (EConstr.mkVar id, NoBindings) in
   let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in 
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 64e023c68a..18461c0533 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -15,6 +15,7 @@ open Util
 open Names
 open Term
 open Constr
+open Context
 open Vars
 open Locus
 open Printer
@@ -136,7 +137,7 @@ let newssrcongrtac arg ist gl =
   (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist)
   (fun () ->
     let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in
-    let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in
+    let arrow = EConstr.mkArrow lhs Sorts.Relevant (EConstr.Vars.lift 1 rhs) in
     tclMATCH_GOAL (arrow, gl') (fun gl' -> [|fs gl' lhs;fs gl' rhs|])
     (fun lr -> tclTHEN (Proofview.V82.of_tactic (Tactics.apply (ssr_congr lr))) (congrtac (arg, mkRType) ist))
     (fun _ _ -> errorstrm Pp.(str"Conclusion is not an equality nor an arrow")))
@@ -335,7 +336,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
     let (sigma, ev) = Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
     (sigma, ev)
   in
-  let pred = EConstr.mkNamedLambda pattern_id rdx_ty pred in
+  let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in
   let elim, gl = 
     let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
     let sort = elimination_sort_of_goal gl in
@@ -362,7 +363,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
         let names = let rec aux t = function 0 -> [] | n ->
           let t = Reductionops.whd_all env sigma t in
           match EConstr.kind_of_type sigma t with
-          | ProdType (name, _, t) -> name :: aux t (n-1)
+          | ProdType (name, _, t) -> name.binder_name :: aux t (n-1)
           | _ -> assert false in aux hd_ty (Array.length args) in
         hd_ty, Util.List.map_filter (fun (t, name) ->
           let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in
@@ -403,7 +404,7 @@ let rwcltac cl rdx dir sr gl =
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
           pirrel_rewrite cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
       | _ -> 
-          let cl' = EConstr.mkApp (EConstr.mkNamedLambda pattern_id rdxt cl, [|rdx|]) in
+          let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
           let sigma, _ = Typing.type_of env sigma cl' in
           let gl = pf_merge_uc_of sigma gl in
           Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl
@@ -413,8 +414,8 @@ let rwcltac cl rdx dir sr gl =
         try EConstr.destCast (project gl) r2 with _ ->
         errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr))
                     ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in
-      let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
-      let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in
+      let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
+      let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in
       let itacs = [introid pattern_id; introid rule_id] in
       let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in
       let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in
@@ -426,7 +427,9 @@ let rwcltac cl rdx dir sr gl =
       if occur_existential (project gl) (Tacmach.pf_concl gl)
       then errorstrm Pp.(str "Rewriting impacts evars")
       else errorstrm Pp.(str "Dependent type error in rewrite of "
-        ++ pr_constr_env (pf_env gl) (project gl) (Term.mkNamedLambda pattern_id (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl)))
+        ++ pr_constr_env (pf_env gl) (project gl)
+          (Term.mkNamedLambda (make_annot pattern_id Sorts.Relevant)
+             (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl)))
   in
   tclTHEN cvtac' rwtac gl
 
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 8c1363020a..9ea35b8694 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -13,6 +13,7 @@
 open Pp
 open Names
 open Constr
+open Context
 open Tacmach
 
 open Ssrmatching_plugin.Ssrmatching
@@ -54,7 +55,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
   let c, (gl, cty) =  match EConstr.kind sigma c with
   | Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
   | _ -> c, pfe_type_of gl c in
-  let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in
+  let cl' = EConstr.mkLetIn (make_annot (Name id) Sorts.Relevant, c, cty, cl) in
   Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl
 
 open Util
@@ -162,7 +163,7 @@ let havetac ist
      let assert_is_conv gl =
        try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl
        with _ -> errorstrm (str "Given proof term is not of type " ++
-         pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in
+         pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) Sorts.Relevant concl)) in
      gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c
    | FwdHave, false, false ->
      let skols = List.flatten (List.map (function
@@ -190,10 +191,10 @@ let havetac ist
             Proofview.V82.of_tactic (unfold [abstract; abstract_key]) gl))
    | _,true,true  ->
      let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in
-     gl, EConstr.mkArrow ty concl, hint, itac, clr
+     gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, itac, clr
    | _,false,true ->
      let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in
-     gl, EConstr.mkArrow ty concl, hint, id, itac_c
+     gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, id, itac_c
    | _, false, false -> 
      let n, cty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in
      gl, cty, Tacticals.tclTHEN (binderstac n) hint, id, Tacticals.tclTHEN itac_c simpltac
@@ -233,7 +234,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
     let gens = List.filter (function _, Some _ -> true | _ -> false) gens in
     let concl = pf_concl gl in
     let c = EConstr.mkProp in
-    let c = if cut_implies_goal then EConstr.mkArrow c concl else c in
+    let c = if cut_implies_goal then EConstr.mkArrow c Sorts.Relevant concl else c in
     let gl, args, c = List.fold_right mkabs gens (gl,[],c) in
     let env, _ =
       List.fold_left (fun (env, c) _ ->
@@ -245,10 +246,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
     let fake_gl = {Evd.it = k; Evd.sigma = sigma} in
     let _, ct, _, uc = pf_interp_ty ist fake_gl ct in
     let rec var2rel c g s = match EConstr.kind sigma c, g with
-      | Prod(Anonymous,_,c), [] -> EConstr.mkProd(Anonymous, EConstr.Vars.subst_vars s ct, c)
+      | Prod({binder_name=Anonymous} as x,_,c), [] -> EConstr.mkProd(x, EConstr.Vars.subst_vars s ct, c)
       | Sort _, [] -> EConstr.Vars.subst_vars s ct
-      | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s))
-      | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s))
+      | LetIn({binder_name=Name id} as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s))
+      | Prod({binder_name=Name id} as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s))
       | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in
     let c = var2rel c gens [] in
     let rec pired c = function
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index a8dfd69240..e9fe1f3e48 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -13,6 +13,7 @@ open Ssrmatching_plugin
 open Util
 open Names
 open Constr
+open Context
 
 open Proofview
 open Proofview.Notations
@@ -393,12 +394,12 @@ let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
       let sigma, m = Evarutil.new_evar env sigma abstract_ty in
       sigma, (m, abstract_ty) in
     let sigma, kont =
-      let rd = Context.Rel.Declaration.LocalAssum (Name id, abstract_ty) in
+      let rd = Context.Rel.Declaration.LocalAssum (make_annot (Name id) Sorts.Relevant, abstract_ty) in
       let sigma, ev = Evarutil.new_evar (EConstr.push_rel rd env) sigma concl in
       sigma, ev
     in
     let term =
-      EConstr.(mkApp (mkLambda(Name id,abstract_ty,kont),[|abstract_proof|])) in
+      EConstr.(mkApp (mkLambda(make_annot (Name id) Sorts.Relevant,abstract_ty,kont),[|abstract_proof|])) in
     let sigma, _ = Typing.type_of env sigma term in
     sigma, term
   end in
@@ -608,7 +609,7 @@ let with_defective maintac deps clr = Goal.enter begin fun g ->
   let sigma, concl = Goal.(sigma g, concl g) in
   let top_id =
     match EConstr.kind_of_type sigma concl with
-    | Term.ProdType (Name id, _, _)
+    | Term.ProdType ({binder_name=Name id}, _, _)
       when Ssrcommon.is_discharged_id id -> id
     | _ -> Ssrcommon.top_id in
   let top_gen = Ssrequality.mkclr clr, Ssrmatching.cpattern_of_id top_id in
@@ -683,7 +684,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
            let name = Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) in
 
            let new_concl =
-             mkProd (Name name, case_ty, mkArrow refl (Vars.lift 2 concl)) in
+             mkProd (make_annot (Name name) Sorts.Relevant, case_ty, mkArrow refl Sorts.Relevant (Vars.lift 2 concl)) in
            let erefl, sigma = mkCoqRefl case_ty case env sigma in
            Proofview.Unsafe.tclEVARS sigma <*>
            Tactics.apply_type ~typecheck:true new_concl [case;erefl]
@@ -707,7 +708,7 @@ let mkEq dir cl c t n env sigma =
   eqargs.(Ssrequality.dir_org dir) <- mkRel n;
   let eq, sigma = mkCoqEq env sigma in
   let refl, sigma = mkCoqRefl t c env sigma in
-  mkArrow (mkApp (eq, eqargs)) (Vars.lift 1 cl), refl, sigma
+  mkArrow (mkApp (eq, eqargs)) Sorts.Relevant (Vars.lift 1 cl), refl, sigma
 
 (** in [tac/v: last gens..] the first (last to be run) generalization is
     "special" in that is it also the main argument of [tac] and is eventually
@@ -743,7 +744,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
           Ssrcommon.errorstrm Pp.(str "@ can be used with let-ins only")
       | Context.Named.Declaration.LocalDef (name, b, ty) ->
           Unsafe.tclEVARS sigma <*>
-          tclUNIT (true, EConstr.mkLetIn (Name name,b,ty,cl), c, clr)
+          tclUNIT (true, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl), c, clr)
     else
       Unsafe.tclEVARS sigma <*>
       Ssrcommon.tacMKPROD c cl >>= fun ccl ->
@@ -757,7 +758,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
       Unsafe.tclEVARS sigma <*>
       Ssrcommon.tacTYPEOF p >>= fun pty ->
       (* TODO: check bug: cl0 no lift? *)
-      let ccl = EConstr.mkProd (Ssrcommon.constr_name sigma c, pty, cl0) in
+      let ccl = EConstr.mkProd (make_annot (Ssrcommon.constr_name sigma c) Sorts.Relevant, pty, cl0) in
       tclUNIT (false, ccl, p, clr)
   else
     Ssrcommon.errorstrm Pp.(str "generalized term didn't match")
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index f12f9fac0f..bbe7bde78b 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -12,6 +12,7 @@
 
 open Names
 open Constr
+open Context
 open Termops
 open Tacmach
 
@@ -102,10 +103,10 @@ let endclausestac id_map clseq gl_id cl0 gl =
     forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in
   let rec unmark c = match EConstr.kind (project gl) c with
   | Var id when hidden_clseq clseq && id = gl_id -> cl0
-  | Prod (Name id, t, c') when List.mem_assoc id id_map ->
-    EConstr.mkProd (Name (orig_id id), unmark t, unmark c')
-  | LetIn (Name id, v, t, c') when List.mem_assoc id id_map ->
-    EConstr.mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c')
+  | Prod ({binder_name=Name id} as na, t, c') when List.mem_assoc id id_map ->
+    EConstr.mkProd ({na with binder_name=Name (orig_id id)}, unmark t, unmark c')
+  | LetIn ({binder_name=Name id} as na, v, t, c') when List.mem_assoc id id_map ->
+    EConstr.mkLetIn ({na with binder_name=Name (orig_id id)}, unmark v, unmark t, unmark c')
   | _ -> EConstr.map (project gl) unmark c in
   let utac hyp =
     Proofview.V82.of_tactic 
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 2794696017..537fd7d7b4 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -10,6 +10,7 @@
 
 open Util
 open Names
+open Context
 
 open Ltac_plugin
 
@@ -95,7 +96,7 @@ let vsBOOTSTRAP = Goal.enter_one ~__LOC__ begin fun gl ->
   let concl = Goal.concl gl in
   let id = (* We keep the orig name for checks in "in" tcl *)
     match EConstr.kind_of_type (Goal.sigma gl) concl with
-    | Term.ProdType(Name.Name id, _, _)
+    | Term.ProdType({binder_name=Name.Name id}, _, _)
       when Ssrcommon.is_discharged_id id -> id
     | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in
   let view = EConstr.mkVar id in