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, 152 insertions, 120 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 6fd2f7c2bc..34283c49c3 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -2,6 +2,7 @@ open Printer
 open CErrors
 open Util
 open Constr
+open Context
 open EConstr
 open Vars
 open Namegen
@@ -302,7 +303,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
     in
     let old_context_length = List.length context + 1 in
     let witness_fun =
-      mkLetIn(Anonymous,make_refl_eq constructor t1_typ (fst t1),t,
+      mkLetIn(make_annot Anonymous Sorts.Relevant,make_refl_eq constructor t1_typ (fst t1),t,
 	       mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i)))
 	      )
     in
@@ -312,7 +313,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	   try
 	     let witness = Int.Map.find i sub in
 	     if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
-	     (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
+      (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_annot decl,
+                                            witness, RelDecl.get_type decl, witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
@@ -428,7 +430,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
     else if isProd sigma type_of_hyp
     then
       begin
-	let (x,t_x,t') = destProd sigma type_of_hyp in
+        let (x,t_x,t') = destProd sigma type_of_hyp in
 	let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in
 	if is_property sigma ptes_infos t_x actual_real_type_of_hyp then
 	  begin
@@ -541,7 +543,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		(scan_type new_context new_t')
 	    with NoChange ->
 	      (* Last thing todo : push the rel in the context and continue *)
-	      scan_type (LocalAssum (x,t_x) :: context) t'
+              scan_type (LocalAssum (x,t_x) :: context) t'
 	  end
       end
     else
@@ -610,7 +612,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 		   anomaly (Pp.str "cannot compute new term value.")
 	   in
 	 let fun_body =
-	   mkLambda(Anonymous,
+           mkLambda(make_annot Anonymous Sorts.Relevant,
 		    pf_unsafe_type_of g' term,
 		    Termops.replace_term (project g') term (mkRel 1) dyn_infos.info
 		   )
@@ -736,7 +738,7 @@ let build_proof
 		    g
 	      in
 	      build_proof do_finalize_t {dyn_infos with info = t} g
-	  | Lambda(n,t,b) ->
+          | Lambda(n,t,b) ->
 	      begin
 		match EConstr.kind sigma (pf_concl g) with
 		  | Prod _ ->
@@ -1149,7 +1151,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     let fix_offset = List.length princ_params in
     let ptes_to_fix,infos =
       match EConstr.kind (project g) fbody_with_full_params with
-	| Fix((idxs,i),(names,typess,bodies)) ->
+        | Fix((idxs,i),(names,typess,bodies)) ->
 	    let bodies_with_all_params =
 	      Array.map
 		(fun body ->
@@ -1164,7 +1166,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		(fun i types ->
 		   let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in
 		   { idx = idxs.(i)  - fix_offset;
-		     name = Nameops.Name.get_id (fresh_id names.(i));
+                     name = Nameops.Name.get_id (fresh_id names.(i).binder_name);
 		     types = types;
 		     offset = fix_offset;
 		     nb_realargs =
@@ -1195,9 +1197,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 			 applist(body,List.rev_map var_of_decl full_params))
 		     in
 		     match EConstr.kind (project g) body_with_full_params with
-		       | Fix((_,num),(_,_,bs)) ->
+                       | Fix((_,num),(_,_,bs)) ->
                                Reductionops.nf_betaiota (pf_env g) (project g)
-				 (
+                                 (
 				   (applist
 				      (substl
 					 (List.rev
@@ -1514,7 +1516,7 @@ let is_valid_hypothesis sigma predicates_name =
   let rec is_valid_hypothesis typ =
     is_pte typ ||
       match EConstr.kind sigma typ with
-	| Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
+        | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
 	| _ -> false
   in
   is_valid_hypothesis
@@ -1565,7 +1567,7 @@ let prove_principle_for_gen
   in
   let rec_arg_id =
     match List.rev post_rec_arg with
-      | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id
+      | (LocalAssum ({binder_name=Name id},_) | LocalDef ({binder_name=Name id},_,_)) :: _ -> id
       | _ -> assert false
   in
 (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index ca09cad1f3..1217ba0eba 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -14,6 +14,7 @@ open Term
 open Sorts
 open Util
 open Constr
+open Context
 open Vars
 open Namegen
 open Names
@@ -72,7 +73,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       then List.tl args
       else args
     in
-    Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl),
+    Context.Named.Declaration.LocalAssum (map_annot Nameops.Name.get_id (Context.Rel.Declaration.get_annot decl),
                                           Term.compose_prod real_args (mkSort new_sort))
   in
   let new_predicates =
@@ -137,14 +138,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	| Rel n ->
 	    begin
 	      try match Environ.lookup_rel n env with
-		| LocalAssum (_,t) | LocalDef (_,_,t) when is_dom t -> raise Toberemoved
+                | LocalAssum (_,t) | LocalDef (_,_,t) when is_dom t -> raise Toberemoved
 		| _ -> pre_princ,[]
 	      with Not_found -> assert false
 	    end
-	| Prod(x,t,b) ->
-	    compute_new_princ_type_for_binder remove mkProd env x t b
-	| Lambda(x,t,b) ->
-	    compute_new_princ_type_for_binder  remove mkLambda env x t b
+        | Prod(x,t,b) ->
+            compute_new_princ_type_for_binder remove mkProd env x t b
+        | Lambda(x,t,b) ->
+            compute_new_princ_type_for_binder  remove mkLambda env x t b
 	| Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved
 	| App(f,args) when is_dom f ->
 	    let var_to_be_removed = destRel (Array.last args) in
@@ -164,8 +165,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	    let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
 	    applistc new_f new_args,
 	    list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove
-	| LetIn(x,v,t,b) ->
-	    compute_new_princ_type_for_letin remove env x v t b
+        | LetIn(x,v,t,b) ->
+            compute_new_princ_type_for_letin remove env x v t b
 	| _ -> pre_princ,[]
     in
 (*     let _ = match Constr.kind pre_princ with *)
@@ -181,14 +182,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     begin
       try
 	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
-	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
-	let new_env = Environ.push_rel (LocalAssum (x,t)) env in
+        let new_x = map_annot (get_name (Termops.ids_of_context env)) x in
+        let new_env = Environ.push_rel (LocalAssum (x,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	 if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
 	 then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
 	 else
 	   (
-	     bind_fun(new_x,new_t,new_b),
+             bind_fun(new_x,new_t,new_b),
 	     list_union_eq
 	       Constr.equal
 	       binders_to_remove_from_t
@@ -210,14 +211,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       try
 	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
 	let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in
-	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
-	let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
+        let new_x = map_annot (get_name (Termops.ids_of_context env)) x in
+        let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
 	then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
 	else
 	  (
-	    mkLetIn(new_x,new_v,new_t,new_b),
+            mkLetIn(new_x,new_v,new_t,new_b),
 	    list_union_eq
 	      Constr.equal
 	      (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v)
@@ -250,8 +251,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   it_mkProd_or_LetIn
     (it_mkProd_or_LetIn
-       pre_res (List.map (function Context.Named.Declaration.LocalAssum (id,b)   -> LocalAssum (Name (Hashtbl.find tbl id), b)
-                                 | Context.Named.Declaration.LocalDef (id,t,b) -> LocalDef (Name (Hashtbl.find tbl id), t, b))
+       pre_res (List.map (function
+           | Context.Named.Declaration.LocalAssum (id,b) ->
+             LocalAssum (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, b)
+           | Context.Named.Declaration.LocalDef (id,t,b) ->
+             LocalDef (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, t, b))
           	      new_predicates)
     )
     (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params)
@@ -264,7 +268,7 @@ let change_property_sort evd toSort princ princName =
   let princ_info = compute_elim_sig evd princ in
   let change_sort_in_predicate decl =
     LocalAssum
-    (get_name decl,
+    (get_annot decl,
      let args,ty = decompose_prod (EConstr.Unsafe.to_constr (get_type decl)) in
      let s = destSort ty in
        Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty);
@@ -414,7 +418,7 @@ let get_funs_constant mp =
       | Fix((_,(na,_,_))) ->
 	  Array.mapi
 	    (fun i na ->
-	       match na with
+               match na.binder_name with
 		 | Name id ->
                      let const = Constant.make2 mp (Label.of_id id) in
 		     const,i
@@ -451,7 +455,8 @@ let get_funs_constant mp =
       let first_params = List.hd l_params  in
       List.iter
 	(fun params ->
-	   if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
+   if not (List.equal (fun (n1, c1) (n2, c2) ->
+       eq_annot Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
 	   then user_err Pp.(str "Not a mutal recursive block")
 	)
 	l_params
@@ -461,7 +466,7 @@ let get_funs_constant mp =
       try
 	let extract_info is_first body =
 	  match Constr.kind body with
-	    | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
+            | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
 	    | _ ->
 		if is_first && Int.equal (List.length l_bodies) 1
 		then raise Not_Rec
@@ -469,9 +474,9 @@ let get_funs_constant mp =
 	in
 	let first_infos = extract_info true (List.hd l_bodies) in
 	let check body  = (* Hope this is correct *)
-	  let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
-            Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 &&
-            Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
+          let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
+     Array.equal Int.equal ia1 ia2 && Array.equal (eq_annot Name.equal) na1 na2 &&
+     Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
 	  in
 	  if not (eq_infos first_infos (extract_info false body))
 	  then  user_err Pp.(str "Not a mutal recursive block")
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index ba0a3bbb5c..8611dcaf83 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -2,6 +2,7 @@ open Printer
 open Pp
 open Names
 open Constr
+open Context
 open Vars
 open Glob_term
 open Glob_ops
@@ -343,12 +344,13 @@ let raw_push_named (na,raw_value,raw_typ) env =
   match na with
     | Anonymous -> env
     | Name id ->
-        let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
+      let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
+      let na = make_annot id Sorts.Relevant in (* TODO relevance *)
         (match raw_value with
         | None ->
-           EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env
+           EConstr.push_named (NamedDecl.LocalAssum (na,typ)) env
         | Some value ->
-           EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env)
+           EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env)
 
 
 let add_pat_variables pat typ env : Environ.env =
@@ -356,7 +358,7 @@ let add_pat_variables pat typ env : Environ.env =
     observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
 
     match DAst.get pat with
-      | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
+      | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (make_annot na Sorts.Relevant,typ)) env
       | PatCstr(c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
 	    try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
@@ -375,16 +377,18 @@ let add_pat_variables pat typ env : Environ.env =
            let open Context.Rel.Declaration in
            let sigma, _ = Pfedit.get_current_context () in
            match decl with
-	   | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false
-	   | LocalAssum (Name id, t) ->
+           | LocalAssum ({binder_name=Anonymous},_) | LocalDef ({binder_name=Anonymous},_,_) -> assert false
+           | LocalAssum ({binder_name=Name id} as na, t) ->
+             let na = {na with binder_name=id} in
              let new_t =  substl ctxt t in
              observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
                       str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
                       str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl ()
                      );
              let open Context.Named.Declaration in
-             (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
-           | LocalDef (Name id, v, t) ->
+             (Environ.push_named (LocalAssum (na,new_t)) env,mkVar id::ctxt)
+           | LocalDef ({binder_name=Name id} as na, v, t) ->
+             let na = {na with binder_name=id} in
              let new_t =  substl ctxt t in
              let new_v = substl ctxt v in
              observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
@@ -394,7 +398,7 @@ let add_pat_variables pat typ env : Environ.env =
                       str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl ()
                      );
              let open Context.Named.Declaration in
-             (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
+             (Environ.push_named (LocalDef (na,new_v,new_t)) env,mkVar id::ctxt)
         )
 	(Environ.rel_context new_env)
 	~init:(env,[])
@@ -626,11 +630,12 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
         let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
+        let v_r = Sorts.Relevant in (* TODO relevance *)
 	let new_env =
 	  match n with
 	      Anonymous -> env
-            | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env
-	in
+            | Name id -> EConstr.push_named (NamedDecl.LocalDef (make_annot id v_r,v_as_constr,v_type)) env
+        in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_letin n) v_res b_res
     | GCases(_,_,el,brl) ->
@@ -939,9 +944,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			let new_t =
 			  mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
 			in
-			let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
-                        let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
-			let new_b,id_to_exclude =
+                        let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
+                        let r = Sorts.Relevant in (* TODO relevance *)
+                        let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+                        let new_b,id_to_exclude =
 			  rebuild_cons new_env
 			    nb_args relname
 			    args new_crossed_types
@@ -974,9 +980,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let new_args = List.map (replace_var_by_term id rt) args in
 		    let subst_b =
 		      if is_in_b then b else  replace_var_by_term id rt b
-		    in
-                    let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
-		    let new_b,id_to_exclude =
+                    in
+                    let r = Sorts.Relevant in (* TODO relevance *)
+                    let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+                    let new_b,id_to_exclude =
 		      rebuild_cons
 			new_env
 			nb_args relname
@@ -1057,8 +1064,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    let new_env =
 		      let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
-                      EConstr.push_rel (LocalAssum (n,t')) env
-		    in
+                      let r = Sorts.Relevant in (* TODO relevance *)
+                      EConstr.push_rel (LocalAssum (make_annot n r,t')) env
+                    in
 		    let new_b,id_to_exclude =
 		      rebuild_cons
 			new_env
@@ -1095,8 +1103,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      with Continue -> 
                 observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
 		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-                let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
-		let new_b,id_to_exclude =
+                let r = Sorts.Relevant in (* TODO relevance *)
+                let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+                let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
 		    args new_crossed_types
@@ -1111,8 +1120,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	    | _ ->
                 observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
 		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-                let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
-		let new_b,id_to_exclude =
+                let r = Sorts.Relevant in (* TODO relevance *)
+                let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+                let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
 		    args new_crossed_types
@@ -1132,8 +1142,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let t',ctx = Pretyping.understand env (Evd.from_env env) t in
 	  match n with
 	    | Name id ->
-                let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
-		let new_b,id_to_exclude =
+              let r = Sorts.Relevant in (* TODO relevance *)
+              let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
+                let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
 		    (args@[mkGVar id])new_crossed_types
@@ -1158,7 +1169,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
           let type_t' = Typing.unsafe_type_of env evd t' in
           let t' = EConstr.Unsafe.to_constr t' in
 	  let type_t' = EConstr.Unsafe.to_constr type_t' in
-	  let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in
+          let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
 	      nb_args relname
@@ -1182,8 +1193,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      depth t
 	  in
 	  let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
-          let new_env = EConstr.push_rel (LocalAssum (na,t')) env in
-	  let new_b,id_to_exclude =
+          let r = Sorts.Relevant in (* TODO relevance *)
+          let new_env = EConstr.push_rel (LocalAssum (make_annot na r,t')) env in
+          let new_b,id_to_exclude =
 	    rebuild_cons new_env
 	      nb_args relname
 	      args (t::crossed_types)
@@ -1320,7 +1332,7 @@ let do_build_inductive
        let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in
        let t = EConstr.Unsafe.to_constr t in
        evd,
-       Environ.push_named (LocalAssum (id,t))
+       Environ.push_named (LocalAssum (make_annot id Sorts.Relevant,t))
 			 env
       )
       funnames
@@ -1364,7 +1376,8 @@ let do_build_inductive
     Util.Array.fold_left2 (fun env rel_name rel_ar ->
         let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in
         let rex = EConstr.Unsafe.to_constr rex in
-        Environ.push_named (LocalAssum (rel_name,rex)) env) env relnames rel_arities
+        let r = Sorts.Relevant in (* TODO relevance *)
+        Environ.push_named (LocalAssum (make_annot rel_name r,rex)) env) env relnames rel_arities
   in
   (* and of the real constructors*)
   let constr i res =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 42dc66dcf4..b69ca7080c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -3,6 +3,7 @@ open Sorts
 open Util
 open Names
 open Constr
+open Context
 open EConstr
 open Pp
 open Indfun_common
@@ -49,7 +50,8 @@ let functional_induction with_clean c princl pat =
 		    user_err  (str "Cannot find induction information on "++
                                        Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
 		in
-		match Tacticals.elimination_sort_of_goal g with
+                match Tacticals.elimination_sort_of_goal g with
+                | InSProp -> finfo.sprop_lemma
 		| InProp -> finfo.prop_lemma
 		| InSet -> finfo.rec_lemma
 		| InType -> finfo.rect_lemma
@@ -169,7 +171,8 @@ let build_newrecursive
         let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in
         let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
         let open Context.Named.Declaration in
-        (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
+        let r = Sorts.Relevant in (* TODO relevance *)
+        (EConstr.push_named (LocalAssum (make_annot recname r,arity)) env, Id.Map.add recname impl impls))
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
@@ -621,8 +624,8 @@ let rebuild_bl aux bl typ = rebuild_bl aux bl typ
 
 let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = 
   let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in
-  let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
-  let constr_expr_typel = 
+  let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
+  let constr_expr_typel =
     with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
   let fixpoint_exprl_with_new_bl = 
     List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index cba3cc3d42..88546e9ae8 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -199,6 +199,7 @@ type function_info =
       rect_lemma : Constant.t option;
       rec_lemma : Constant.t option;
       prop_lemma : Constant.t option;
+      sprop_lemma : Constant.t option;
       is_general : bool; (* Has this function been defined using general recursive definition *)
     }
 
@@ -249,6 +250,7 @@ let subst_Function (subst,finfos) =
   let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in
   let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in
   let prop_lemma' =  Option.Smart.map do_subst_con finfos.prop_lemma in
+  let sprop_lemma' = Option.Smart.map do_subst_con finfos.sprop_lemma in
   if function_constant' == finfos.function_constant &&
     graph_ind' == finfos.graph_ind &&
     equation_lemma' == finfos.equation_lemma &&
@@ -256,7 +258,8 @@ let subst_Function (subst,finfos) =
     completeness_lemma' == finfos.completeness_lemma &&
     rect_lemma' == finfos.rect_lemma &&
     rec_lemma' == finfos.rec_lemma &&
-    prop_lemma' == finfos.prop_lemma
+    prop_lemma' == finfos.prop_lemma &&
+    sprop_lemma' == finfos.sprop_lemma
   then finfos
   else
     { function_constant = function_constant';
@@ -267,6 +270,7 @@ let subst_Function (subst,finfos) =
       rect_lemma = rect_lemma' ;
       rec_lemma = rec_lemma';
       prop_lemma = prop_lemma';
+      sprop_lemma = sprop_lemma';
       is_general = finfos.is_general
     }
 
@@ -333,6 +337,7 @@ let add_Function is_general f =
   and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect")
   and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
+  and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
     with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
@@ -345,6 +350,7 @@ let add_Function is_general f =
       rect_lemma = rect_lemma;
       rec_lemma = rec_lemma;
       prop_lemma = prop_lemma;
+      sprop_lemma = sprop_lemma;
       graph_ind = graph_ind;
       is_general = is_general
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1e0b95df34..4ec3131518 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -70,6 +70,7 @@ type function_info =
       rect_lemma : Constant.t option;
       rec_lemma : Constant.t option;
       prop_lemma : Constant.t option;
+      sprop_lemma : Constant.t option;
       is_general : bool;
     }
 
@@ -109,9 +110,9 @@ val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_referenc
 val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic
 
 val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
-  (Names.Name.t * EConstr.t) list * EConstr.t
-val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
-val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
+  (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
+val compose_lam : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t
+val compose_prod : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t
 
 type tcc_lemma_value =
   | Undefined
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 95e2e9f6e5..37dbfec4c9 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -15,6 +15,7 @@ open Util
 open Names
 open Term
 open Constr
+open Context
 open EConstr
 open Vars
 open Pp
@@ -142,12 +143,13 @@ let generate_type evd g_to_f f graph i =
     \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,  \]
     i*)
   let pre_ctxt =
-    LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt
+    LocalAssum (make_annot (Name res_id) Sorts.Relevant, lift 1 res_type) ::
+    LocalDef (make_annot (Name fv_id) Sorts.Relevant, mkApp (f,args_as_rels), res_type) :: fun_ctxt
   in
   (*i and we can return the solution depending on which lemma type we are defining i*)
   if g_to_f
-  then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
-  else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
+  then LocalAssum (make_annot Anonymous Sorts.Relevant,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
+  else LocalAssum (make_annot Anonymous Sorts.Relevant,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
 
 
 (*
@@ -270,10 +272,10 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
 	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
 	     let sigma = project g in
 	     match EConstr.kind sigma type_of_hid with
-	       | Prod(_,_,t') ->
+               | Prod(_,_,t') ->
 		   begin
 		     match EConstr.kind sigma t' with
-		       | Prod(_,t'',t''') ->
+                       | Prod(_,t'',t''') ->
 			   begin
 			     match EConstr.kind sigma t'',EConstr.kind sigma t''' with
 			       | App(eq,args), App(graph',_)
@@ -358,17 +360,16 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
     (* end of branche proof *)
     let lemmas =
       Array.map
-	(fun ((_,(ctxt,concl))) ->
-	   match ctxt with
-	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.")
-	     | hres::res::decl::ctxt ->
-		let res = EConstr.it_mkLambda_or_LetIn
-			    (EConstr.it_mkProd_or_LetIn concl [hres;res])
-			    (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt)
-		in
-		res
-	)
-	lemmas_types_infos
+        (fun ((_,(ctxt,concl))) ->
+           match ctxt with
+           | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.")
+           | hres::res::decl::ctxt ->
+             let res = EConstr.it_mkLambda_or_LetIn
+                 (EConstr.it_mkProd_or_LetIn concl [hres;res])
+                 (LocalAssum (RelDecl.get_annot decl, RelDecl.get_type decl) :: ctxt)
+             in
+             res)
+        lemmas_types_infos
     in
     let param_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar param_names in
@@ -429,7 +430,7 @@ let generalize_dependent_of x hyp g =
   let open Context.Named.Declaration in
   tclMAP
     (function
-       | LocalAssum (id,t) when not (Id.equal id hyp) &&
+       | LocalAssum ({binder_name=id},t) when not (Id.equal id hyp) &&
 	   (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
@@ -456,7 +457,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
     let eq_ind = make_eq () in
     let sigma = project g in
     match EConstr.kind sigma (pf_concl g) with
-	  | Prod(_,t,t') ->
+          | Prod(_,t,t') ->
 	      begin
 		match EConstr.kind sigma t with
 		  | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind)  ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8746c37309..988cae8fbf 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -12,6 +12,7 @@
 module CVars = Vars
 
 open Constr
+open Context
 open EConstr
 open Vars
 open Namegen
@@ -182,7 +183,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
       )
     in
     let context = List.map
-      (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al))
+      (fun (x, c) -> LocalAssum (make_annot (Name x) Sorts.Relevant, c)) (List.combine rev_x_id_l (List.rev al))
     in
     let env = Environ.push_rel_context context (Global.env ()) in
     let glob_body =
@@ -388,9 +389,9 @@ let add_vars sigma forbidden e =
 let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = 
   fun g -> 
     let rev_context,b = decompose_lam_n (project g) nb_lam e in
-    let ids = List.fold_left (fun acc (na,_) -> 	
+    let ids = List.fold_left (fun acc (na,_) ->
       let pre_id = 
-	match na with 
+        match na.binder_name with
 	  | Name x -> x 
 	  | Anonymous -> ano_id 
       in
@@ -433,10 +434,10 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
   match EConstr.kind sigma expr_info.info with 
     | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
     | Proj _ -> user_err Pp.(str "Function cannot treat projections")
-    | LetIn(na,b,t,e) -> 
+    | LetIn(na,b,t,e) ->
       begin
 	let new_continuation_tac = 
-	  jinfo.letiN (na,b,t,e) expr_info continuation_tac
+          jinfo.letiN (na.binder_name,b,t,e) expr_info continuation_tac
 	in
 	travel jinfo new_continuation_tac 
 	  {expr_info with info = b; is_final=false} g
@@ -450,7 +451,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
 	with e when CErrors.noncritical e ->
           user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
       end
-    | Lambda(n,t,b) -> 
+    | Lambda(n,t,b) ->
       begin
 	try
 	  check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
@@ -853,8 +854,8 @@ let rec prove_le g =
           EConstr.is_global sigma (le ()) c
         | _ -> false
         in
-	let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
-	in 
+        let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in
+        let h = h.binder_name in
 	let y = 
 	  let _,args = decompose_app sigma t in 
 	  List.hd (List.tl args)
@@ -877,10 +878,10 @@ let rec make_rewrite_list expr_info max = function
           let sigma = project g in
 	  let t_eq = compute_renamed_type g (mkVar hp) in
 	  let k,def =
-	    let k_na,_,t = destProd sigma t_eq in
-	    let _,_,t  = destProd sigma t in
-	    let def_na,_,_ = destProd sigma t in
-	    Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
+            let k_na,_,t = destProd sigma t_eq in
+            let _,_,t  = destProd sigma t in
+            let def_na,_,_ = destProd sigma t in
+            Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name
 	  in
 	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
@@ -903,10 +904,10 @@ let make_rewrite expr_info l hp max =
           let sigma = project g in
 	  let t_eq = compute_renamed_type g (mkVar hp) in
 	  let k,def =
-	    let k_na,_,t = destProd sigma t_eq in
-	    let _,_,t  = destProd sigma t in
-	    let def_na,_,_ = destProd sigma t in
-	    Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
+            let k_na,_,t = destProd sigma t_eq in
+            let _,_,t  = destProd sigma t in
+            let def_na,_,_ = destProd sigma t in
+            Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name
 	  in
 	 observe_tac (str "general_rewrite_bindings")
 	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
@@ -1054,20 +1055,19 @@ let compute_terminate_type nb_args func =
   let right = mkRel 5 in
   let delayed_force c = EConstr.Unsafe.to_constr (delayed_force c) in
   let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in
-  let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in
+  let result = (mkProd (make_annot (Name def_id) Sorts.Relevant, lift 4 a_arrow_b, equality)) in
   let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in
   let nb_iter =
     mkApp(delayed_force ex,
 	  [|delayed_force nat;
 	    (mkLambda
-	       (Name
-		  p_id,
+               (make_annot (Name p_id) Sorts.Relevant,
 		  delayed_force nat,
-		  (mkProd (Name k_id, delayed_force nat,
-			   mkArrow cond result))))|])in
+                  (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat,
+                           mkArrow cond Sorts.Relevant result))))|])in
   let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref),
 		    [|b;
-		      (mkLambda (Name v_id, b, nb_iter))|]) in
+                      (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in
   compose_prod rev_args value
 
 
@@ -1165,15 +1165,15 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
       let func_body = EConstr.of_constr func_body in
       let (f_name, _, body1) = destLambda sigma func_body in
       let f_id =
-	match f_name with
+        match f_name.binder_name with
 	  | Name f_id -> next_ident_away_in_goal f_id ids
 	  | Anonymous -> anomaly (Pp.str "Anonymous function.")
       in
       let n_names_types,_ = decompose_lam_n sigma nb_args body1 in
       let n_ids,ids =
 	List.fold_left
-	  (fun (n_ids,ids) (n_name,_) ->
-	     match n_name with
+          (fun (n_ids,ids) (n_name,_) ->
+             match n_name.binder_name with
 	       | Name id ->
 		   let n_id = next_ident_away_in_goal id ids in
 		   n_id::n_ids,n_id::ids
@@ -1270,12 +1270,12 @@ let is_rec_res id =
 let clear_goals sigma =
   let rec clear_goal t =
     match EConstr.kind sigma t with
-      | Prod(Name id as na,t',b) ->
+      | Prod({binder_name=Name id} as na,t',b) ->
 	  let b' = clear_goal b in
 	  if noccurn sigma 1 b' && (is_rec_res id)
 	  then Vars.lift (-1) b'
 	  else if b' == b then t
-	  else mkProd(na,t',b')
+          else mkProd(na,t',b')
       | _ -> EConstr.map sigma clear_goal t
   in
   List.map clear_goal
@@ -1519,7 +1519,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let env = Global.env() in
   let evd = Evd.from_env env in
   let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in
-  let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
+  let function_r = Sorts.Relevant in (* TODO relevance *)
+  let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot function_name function_r,function_type)) env in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
   let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in
   let evd = Evd.minimize_universes evd in
@@ -1537,7 +1538,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 (*     Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
     match Constr.kind eq' with
       | App(e,[|_;_;eq_fix|]) ->
-	  mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars  eq_fix))
+          mkLambda (make_annot (Name function_name) Sorts.Relevant,function_type,subst_var function_name (compose_lam res_vars  eq_fix))
       | _ -> failwith "Recursive Definition (res not eq)"
   in
   let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in