CLEANUP: Context.{Rel,Named}.Declaration.t

  Originally, rel-context was represented as:

    Context.rel_context = Names.Name.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
                  | LocalDef of Names.Name.t * Constr.t * Constr.t

  Originally, named-context was represented as:

    Context.named_context = Names.Id.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Named.t = LocalAssum of Names.Id.t * Constr.t
                    | LocalDef of Names.Id.t * Constr.t * Constr.t

Motivation:

  (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
      function which looked like this:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      Suppose that you do not know about rel-context and named-context.
      (that is the case of people who just started to read the source code)
      Merlin would tell you that the type of the value you are destructing
      by "match" is:

        'a * 'b option * Constr.t                    (* worst-case scenario *)

      or

        Named.Name.t * Constr.t option * Constr.t    (* best-case scenario (?) *)

      To me, this is akin to wearing an opaque veil.
      It is hard to figure out the meaning of the values you are looking at.
      In particular, it is hard to discover the connection between the value
      we are destructing above and the datatypes and functions defined
      in the "kernel/context.ml" file.

      In this case, the connection is there, but it is not visible
      (between the function above and the "Context" module).

      ------------------------------------------------------------------------

      Now consider, what happens when the reader see the same function
      presented in the following form:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
      to jump to the corresponding definition and learn more.

      In this case, the connection is there, and it is directly visible
      (between the function above and the "Context" module).

  (2) Also, if we already have the concepts such as:
      - local declaration
      - local assumption
      - local definition
      and we describe these notions meticulously in the Reference Manual,
      then it is a real pity not to reinforce the connection
      of the actual code with the abstract description we published.

21 files changed, 205 insertions, 158 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc3d9ed56..359157a4c 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -824,7 +824,7 @@ let __eps__ = Id.of_string "_eps_"
 let new_state_var typ state =
   let id = pf_get_new_id __eps__ state.gls in
   let {it=gl ; sigma=sigma} = state.gls in
-  let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in
+  let gls = Goal.V82.new_goal_with sigma gl [Context.Named.Declaration.LocalAssum (id,typ)] in
     state.gls<- gls;
     id
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 09d9cf019..e5b68af8e 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -23,6 +23,7 @@ open Pp
 open Errors
 open Util
 open Proofview.Notations
+open Context.Rel.Declaration
 
 let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
@@ -152,7 +153,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
-	  quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff
+	  quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff
     | _ ->  
 	let patts=patterns_of_constr env sigma nrels term in
 	    `Rule patts
@@ -167,7 +168,7 @@ let litteral_of_constr env sigma term=
 	else
 	  begin
 	    try 
-	      quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff  
+	      quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff
 	    with Not_found ->
 	      `Other (decompose_term env sigma term)
 	  end
@@ -188,7 +189,8 @@ let make_prb gls depth additionnal_terms =
 	 let t = decompose_term env sigma c in
 	   ignore (add_term state t)) additionnal_terms;
     List.iter
-      (fun (id,_,e) ->
+      (fun decl ->
+         let (id,_,e) = Context.Named.Declaration.to_tuple decl in
 	 begin
 	   let cid=mkVar id in
 	   match litteral_of_constr env sigma e with
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 2a44dca21..7cfca53c5 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -403,7 +403,7 @@ let interp_suffices_clause env sigma (hyps,cot)=
     match hyp with
 	(Hprop st | Hvar st) ->
 	  match st.st_label with
-	      Name id -> Environ.push_named (id,None,st.st_it) env0
+	      Name id -> Environ.push_named (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0
 	    | _ -> env in
   let nenv = List.fold_right push_one locvars env in
     nenv,res
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index acee3d6c2..f9399d682 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -116,7 +116,7 @@ let get_top_stack pts =
 let get_stack pts = Proof.get_at_focus proof_focus pts
 
 let get_last env = match Environ.named_context env with
-  | (id,_,_)::_ -> id
+  | decl :: _ -> Context.Named.Declaration.get_id decl
   | [] -> error "no previous statement to use"
 
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index f47b35541..22a646b3f 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -30,6 +30,7 @@ open Namegen
 open Goptions
 open Misctypes
 open Sigma.Notations
+open Context.Named.Declaration
 
 (* Strictness option *)
 
@@ -229,7 +230,8 @@ let close_previous_case pts =
 (* automation *)
 
 let filter_hyps f gls =
-  let filter_aux (id,_,_) =
+  let filter_aux id =
+    let id = get_id id in
     if f id then
       tclIDTAC
     else
@@ -331,11 +333,12 @@ let enstack_subsubgoals env se stack gls=
 	    let rc,_ = Reduction.dest_prod env apptype in
 	    let rec meta_aux last lenv = function
 		[] -> (last,lenv,[])
-	      | (nam,_,typ)::q ->
+	      | decl::q ->
 		  let nlast=succ last in
 		  let (llast,holes,metas) =
 		    meta_aux nlast (mkMeta nlast :: lenv) q in
-		    (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in
+                    let open Context.Rel.Declaration in
+		    (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in
 	    let (nlast,holes,nmetas) =
 		meta_aux se.se_last_meta [] (List.rev rc) in
 	    let refiner = applist (appterm,List.rev holes) in
@@ -411,7 +414,7 @@ let concl_refiner metas body gls =
 	let _A = subst_meta subst typ in
 	let x = id_of_name_using_hdchar env _A Anonymous in
 	let _x = fresh_id avoid x gls in
-	let nenv = Environ.push_named (_x,None,_A) env in
+	let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
 	let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in
 	let nsubst = (n,mkVar _x)::subst in
 	  if List.is_empty rest then
@@ -606,7 +609,7 @@ let assume_tac hyps gls =
        tclTHEN
 	 (push_intro_tac
 	    (fun id ->
-	       Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
+	       Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label))
 	 hyps tclIDTAC gls
 
 let assume_hyps_or_theses hyps gls =
@@ -616,7 +619,7 @@ let assume_hyps_or_theses hyps gls =
 	   tclTHEN
 	     (push_intro_tac
 		(fun id ->
-		   Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam)
+		   Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,c)))) nam)
        | Hprop {st_label=nam;st_it=Thesis (tk)} ->
 	   tclTHEN
 	     (push_intro_tac
@@ -628,7 +631,7 @@ let assume_st hyps gls =
     (fun st ->
        tclTHEN
 	 (push_intro_tac
-	    (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
+	    (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label))
 	 hyps tclIDTAC gls
 
 let assume_st_letin hyps gls =
@@ -637,7 +640,7 @@ let assume_st_letin hyps gls =
        tclTHEN
 	 (push_intro_tac
 	    (fun id ->
-	       Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label))
+	       Proofview.V82.of_tactic (convert_hyp (LocalDef (id, fst st.st_it, snd st.st_it)))) st.st_label))
 	 hyps tclIDTAC gls
 
 (* suffices *)
@@ -731,7 +734,7 @@ let rec consider_match may_intro introduced available expected gls =
 	  error "Not enough sub-hypotheses to match statements."
 	    (* should tell which ones *)
     | id::rest_ids,(Hvar st | Hprop st)::rest ->
-	tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it)))
+	tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it))))
 	  begin
 	    match st.st_label with
 		Anonymous ->
@@ -799,8 +802,8 @@ let define_tac id args body gls =
 let cast_tac id_or_thesis typ gls =
   match id_or_thesis with
       This id ->
-	let (_,body,_) = pf_get_hyp gls id in
-	  Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls
+	let body = pf_get_hyp gls id |> get_value in
+	  Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls
     | Thesis (For _ ) ->
 	error "\"thesis for ...\" is not applicable here."
     | Thesis Plain ->
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index a47dc5b2f..5d1551106 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Context.Named.Declaration
+
 let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
     : Safe_typing.private_constants Entries.const_entry_body =
   Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
@@ -32,7 +34,7 @@ let start_deriving f suchthat lemma =
     let open Proofview in
         TCons ( env , sigma , f_type_type , (fun sigma f_type ->
         TCons ( env , sigma , f_type , (fun sigma ef ->
-        let env' = Environ.push_named (f , (Some ef) , f_type) env in
+        let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
         let evdref = ref sigma in
         let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
         TCons ( env' , !evdref , suchthat , (fun sigma _ ->
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 38aef62e1..6c57bc2bb 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -25,6 +25,7 @@ open Globnames
 open Miniml
 open Table
 open Mlutil
+open Context.Rel.Declaration
 (*i*)
 
 exception I of inductive_kind
@@ -74,7 +75,7 @@ type flag = info * scheme
 let rec flag_of_type env t : flag =
   let t = whd_betadeltaiota env none t in
   match kind_of_term t with
-    | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
+    | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
     | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
@@ -247,7 +248,7 @@ let rec extract_type env db j c args =
     | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop
     | Rel n ->
 	(match lookup_rel n env with
-           | (_,Some t,_) -> extract_type env db j (lift n t) args
+           | LocalDef (_,t,_) -> extract_type env db j (lift n t) args
 	   | _ ->
 	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown
@@ -560,7 +561,7 @@ let rec extract_term env mle mlt c args =
 	       put_magic_if magic (MLlam (id, d')))
     | LetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
-	let env' = push_rel (Name id, Some c1, t1) env in
+	let env' = push_rel (LocalDef (Name id, c1, t1)) env in
 	(* We directly push the args inside the [LetIn].
            TODO: the opt_let_app flag is supposed to prevent that *)
 	let args' = List.map (lift 1) args in
@@ -835,7 +836,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 
 let decomp_lams_eta_n n m env c t =
   let rels = fst (splay_prod_n env none n t) in
-  let rels = List.map (fun (id,_,c) -> (id,c)) rels in
+  let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in
   let rels',c = decompose_lam c in
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index ae2d059fa..2ed436c6b 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -15,6 +15,7 @@ open Tacmach
 open Util
 open Declarations
 open Globnames
+open Context.Rel.Declaration
 
 let qflag=ref true
 
@@ -139,8 +140,8 @@ let build_atoms gl metagen side cciterm =
 		  negative:= unsigned :: !negative
 	    end;
 	  let v = ind_hyps 0 i l gl in
-	  let g i _ (_,_,t) =
-	    build_rec env polarity (lift i t) in
+	  let g i _ decl =
+	    build_rec env polarity (lift i (get_type decl)) in
 	  let f l =
 	    List.fold_left_i g (1-(List.length l)) () l in
 	    if polarity && (* we have a constant constructor *)
@@ -150,8 +151,8 @@ let build_atoms gl metagen side cciterm =
       | Exists(i,l)->
 	  let var=mkMeta (metagen true) in
 	  let v =(ind_hyps 1 i l gl).(0) in
-	  let g i _ (_,_,t) =
-	    build_rec (var::env) polarity (lift i t) in
+	  let g i _ decl =
+	    build_rec (var::env) polarity (lift i (get_type decl)) in
 	    List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
@@ -224,7 +225,7 @@ let build_formula side nam typ gl metagen=
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
 		  | Exists (i,l) ->
-		      let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in
+		      let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in
 			Rexists(m,d,trivial)
 		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a717cc91e..797f43f2a 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -22,6 +22,7 @@ open Formula
 open Sequent
 open Names
 open Misctypes
+open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
 	match inst1,inst2 with
@@ -117,7 +118,7 @@ let mk_open_instance id idc gl m t=
     if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id avoid var_id gl) in
       let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
-      let decl = (Name nid,None,c) in
+      let decl = LocalAssum (Name nid,c) in
 	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m [] env evmap [] in
     evmap, decls, revt
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e676a8a93..b0e8f7d25 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -19,6 +19,7 @@ open Formula
 open Sequent
 open Globnames
 open Locus
+open Context.Named.Declaration
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
@@ -34,12 +35,13 @@ let wrap n b continue seq gls=
     if i<=0 then seq else
       match nc with
 	  []->anomaly (Pp.str "Not the expected number of hyps")
-	| ((id,_,typ) as nd)::q->
+	| nd::q->
+            let id = get_id nd in
 	    if occur_var env id (pf_concl gls) ||
 	      List.exists (occur_var_in_decl env id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in
+	      add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in
   let seq1=aux n nc [] in
   let seq2=if b then
     add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 4c0aa6c75..8bc84608e 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -445,7 +445,11 @@ let is_ineq (h,t) =
 ;;
 *)
 
-let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
+let list_of_sign s =
+  let open Context.Named.Declaration in
+  List.map (function LocalAssum (name, typ) -> name, typ
+                   | LocalDef (name, _, typ) -> name, typ)
+           s;;
 
 let mkAppL a =
    let l = Array.to_list a in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4eab5f912..28982c37f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -15,6 +15,7 @@ open Tactics
 open Indfun_common
 open Libnames
 open Globnames
+open Context.Rel.Declaration
 
 (* let msgnl = Pp.msgnl *)
 
@@ -304,11 +305,11 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
     in
     let new_type_of_hyp,ctxt_size,witness_fun =
       List.fold_left_i
-	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
+	(fun i (end_of_type,ctxt_size,witness_fun) decl ->
 	   try
 	     let witness = Int.Map.find i sub in
-	     if not (Option.is_empty b') then anomaly (Pp.str "can not redefine a rel!");
-	     (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
+	     if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
+	     (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
@@ -536,7 +537,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		(scan_type new_context new_t')
 	    with Failure "NoChange" ->
 	      (* Last thing todo : push the rel in the context and continue *)
-	      scan_type ((x,None,t_x)::context) t'
+	      scan_type (LocalAssum (x,t_x) :: context) t'
 	  end
       end
     else
@@ -736,7 +737,8 @@ let build_proof
 		      tclTHEN
 			(Proofview.V82.of_tactic intro)
 			(fun g' ->
-			   let (id,_,_) = pf_last_hyp g' in
+                           let open Context.Named.Declaration in
+			   let id = pf_last_hyp g' |> get_id in
 			   let new_term =
 			     pf_nf_betaiota g'
 			       (mkApp(dyn_infos.info,[|mkVar id|]))
@@ -921,7 +923,9 @@ let generalize_non_dep hyp g =
   let env = Global.env () in
   let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
   let to_revert,_ =
-    Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
+    let open Context.Named.Declaration in
+    Environ.fold_named_context_reverse (fun (clear,keep) decl ->
+      let hyp = get_id decl in
       if Id.List.mem hyp hyps
         || List.exists (Termops.occur_var_in_decl env hyp) keep
 	|| Termops.occur_var env hyp hyp_typ
@@ -936,7 +940,7 @@ let generalize_non_dep hyp g =
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
-let id_of_decl (na,_,_) =  (Nameops.out_name na)
+let id_of_decl decl = Nameops.out_name (get_name decl)
 let var_of_decl decl = mkVar (id_of_decl decl)
 let revert idl =
   tclTHEN
@@ -1044,7 +1048,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
       (
 	fun g' ->
 	  let just_introduced = nLastDecls nb_intro_to_do g' in
-	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
+          let open Context.Named.Declaration in
+	  let just_introduced_id = List.map get_id just_introduced in
 	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))
 		  (revert just_introduced_id) g'
       )
@@ -1069,11 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	 (Name new_id)
       )
     in
-    let fresh_decl =
-      (fun (na,b,t) ->
-	 (fresh_id na,b,t)
-      )
-    in
+    let fresh_decl = map_name fresh_id in
     let princ_info : elim_scheme =
       { princ_info with
 	  params = List.map fresh_decl princ_info.params;
@@ -1120,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	)
     in
     observe (str "full_params := " ++
-	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
 	       full_params
 	    );
     observe (str "princ_params := " ++
-	       prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
@@ -1165,7 +1166,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    in
 	    let pte_to_fix,rev_info =
 	      List.fold_left_i
-		(fun i (acc_map,acc_info) (pte,_,_) ->
+		(fun i (acc_map,acc_info) decl ->
+		   let pte = get_name decl in
 		   let infos = info_array.(i) in
 		   let type_args,_ = decompose_prod infos.types in
 		   let nargs = List.length type_args in
@@ -1259,7 +1261,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		 let args = nLastDecls nb_args g in
 		 let fix_body = fix_info.body_with_param in
 (* 		 observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
-		 let args_id = List.map (fun (id,_,_) -> id) args in
+                 let open Context.Named.Declaration in
+		 let args_id = List.map get_id args in
 		 let dyn_infos =
 		   {
 		     nb_rec_hyps = -100;
@@ -1276,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		       (do_replace evd
 			  full_params
 			  (fix_info.idx + List.length princ_params)
-			  (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params))
+			  (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params))
 			  (all_funs.(fix_info.num_in_block))
 			  fix_info.num_in_block
 			  all_funs
@@ -1317,8 +1320,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    [
 	      tclDO nb_args (Proofview.V82.of_tactic intro);
 	      (fun g -> (* replacement of the function by its body *)
-		 let args = nLastDecls nb_args g in
-		 let args_id = List.map (fun (id,_,_) -> id) args in
+	         let args = nLastDecls nb_args g in
+                 let open Context.Named.Declaration in
+		 let args_id = List.map get_id args in
 		 let dyn_infos =
 		   {
 		     nb_rec_hyps = -100;
@@ -1520,7 +1524,7 @@ let prove_principle_for_gen
       avoid := new_id :: !avoid;
       Name new_id
   in
-  let fresh_decl (na,b,t) = (fresh_id na,b,t) in
+  let fresh_decl = map_name fresh_id in
   let princ_info : elim_scheme =
     { princ_info with
 	params = List.map fresh_decl princ_info.params;
@@ -1550,11 +1554,11 @@ let prove_principle_for_gen
   in
   let rec_arg_id =
     match List.rev post_rec_arg with
-      | (Name id,_,_)::_ -> id
+      | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id
       | _ -> assert false
   in
 (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
-  let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in
+  let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in
   let relation = substl subst_constrs relation in
   let input_type = substl subst_constrs rec_arg_type in
   let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
@@ -1582,7 +1586,7 @@ let prove_principle_for_gen
       )
       g
   in
-  let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
+  let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
      | None -> error "No tcc proof !!"
@@ -1629,7 +1633,7 @@ let prove_principle_for_gen
     [
       observe_tac "start_tac" start_tac;
       h_intros
-	(List.rev_map (fun (na,_,_) -> Nameops.out_name na)
+	(List.rev_map (fun decl -> Nameops.out_name (get_name decl))
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
       (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1667,7 +1671,7 @@ let prove_principle_for_gen
 	 in
 	 let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  acc_rec_arg_id|])) in
 	 let predicates_names =
-	   List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates
+	   List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates
 	 in
 	 let pte_info =
 	   { proving_tac =
@@ -1683,7 +1687,7 @@ let prove_principle_for_gen
 		       is_mes acc_inv fix_id
 
 		       (!tcc_list@(List.map
-			   (fun (na,_,_) -> (Nameops.out_name na))
+			   (fun decl -> (Nameops.out_name (get_name decl)))
 			   (princ_info.args@princ_info.params)
 			)@ ([acc_rec_arg_id])) eqs
 		    )
@@ -1712,7 +1716,7 @@ let prove_principle_for_gen
 	 (* observe_tac "instanciate_hyps_with_args"  *)
 	   (instanciate_hyps_with_args
 	      make_proof
-	      (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches)
+	      (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches)
 	      (List.rev args_ids)
 	   )
 	   gl'
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e2c3bbb97..7a933c04b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -8,6 +8,7 @@ open Names
 open Pp
 open Entries
 open Tactics
+open Context.Rel.Declaration
 open Indfun_common
 open Functional_principles_proofs
 open Misctypes
@@ -32,11 +33,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t)  : Context.Rel.t =
     match predicates with
     | [] -> []
-    |(Name x,v,t)::predicates ->
-       let id =  Namegen.next_ident_away x avoid in
-       Hashtbl.add tbl id x;
-       (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
-    | (Anonymous,_,_)::_ -> anomaly (Pp.str "Anonymous property binder ")
+    | decl :: predicates ->
+       (match Context.Rel.Declaration.get_name decl with
+	| Name x ->
+	   let id = Namegen.next_ident_away x avoid in
+	   Hashtbl.add tbl id x;
+	   set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
+	| Anonymous -> anomaly (Pp.str "Anonymous property binder "))
   in
   let avoid = (Termops.ids_of_context env_with_params ) in
   let princ_type_info =
@@ -46,15 +49,16 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
 (*   observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *)
 (*   observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
-  let change_predicate_sort i (x,_,t) =
+  let change_predicate_sort i decl =
     let new_sort = sorts.(i) in
-    let args,_ = decompose_prod t in
+    let args,_ = decompose_prod (get_type decl) in
     let real_args =
       if princ_type_info.indarg_in_concl
       then List.tl args
       else args
     in
-    Nameops.out_name x,None,compose_prod real_args (mkSort new_sort)
+    Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl),
+                                          compose_prod real_args (mkSort new_sort))
   in
   let new_predicates =
     List.map_i
@@ -69,7 +73,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	   | _ -> error "Not a valid predicate"
 	)
   in
-  let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in
+  let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in
   let is_pte =
     let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in
     fun t ->
@@ -114,7 +118,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	| Rel n ->
 	    begin
 	      try match Environ.lookup_rel n env with
-		| _,_,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
@@ -159,7 +163,7 @@ 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_x : Name.t = get_name (Termops.ids_of_context env) x in
-	let new_env = Environ.push_rel (x,None,t) env 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 (eq_constr (mkRel 1)) binders_to_remove_from_b
 	 then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b
@@ -188,7 +192,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	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 (x,Some v,t) env 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 (eq_constr (mkRel 1)) binders_to_remove_from_b
 	then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b
@@ -227,7 +231,8 @@ 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 (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b)
+       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))
           	      new_predicates)
     )
     princ_type_info.params
@@ -235,10 +240,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 
 
 let change_property_sort evd toSort princ princName =
+  let open Context.Rel.Declaration in
   let princ_info = compute_elim_sig princ in
-  let change_sort_in_predicate (x,v,t) =
-    (x,None,
-     let args,ty = decompose_prod t in
+  let change_sort_in_predicate decl =
+    LocalAssum
+    (get_name decl,
+     let args,ty = decompose_prod (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);
        compose_prod args (mkSort toSort)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 80de8e764..8a0a1a064 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -335,15 +335,17 @@ let raw_push_named (na,raw_value,raw_typ) env =
     | Name id ->
 	let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in
 	let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
-	Environ.push_named (id,value,typ) env
+        let open Context.Named.Declaration in
+	Environ.push_named (of_tuple (id,value,typ)) env
 
 
 let add_pat_variables pat typ env : Environ.env =
   let rec add_pat_variables env pat typ  : Environ.env =
+    let open Context.Rel.Declaration in
     observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
 
     match pat with
-      | PatVar(_,na) -> Environ.push_rel (na,None,typ) env
+      | PatVar(_,na) -> Environ.push_rel (LocalAssum (na,typ)) env
       | PatCstr(_,c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
 	    try Inductiveops.find_rectype env (Evd.from_env env) typ
@@ -351,15 +353,16 @@ let add_pat_variables pat typ env : Environ.env =
 	  in
 	  let constructors = Inductiveops.get_constructors env indf in
 	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
-	  let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
+	  let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in
 	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
   in
   let new_env = add_pat_variables  env pat typ in
   let res =
     fst (
       Context.Rel.fold_outside
-	(fun (na,v,t) (env,ctxt) ->
-	 match na with
+	(fun decl (env,ctxt) ->
+         let _,v,t = Context.Rel.Declaration.to_tuple decl in
+	 match Context.Rel.Declaration.get_name decl with
 	   | Anonymous -> assert false
 	   | Name id ->
 	       let new_t =  substl ctxt t in
@@ -370,7 +373,8 @@ let add_pat_variables pat typ env : Environ.env =
 			  Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
 			  Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
 		       );
-	       (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
+               let open Context.Named.Declaration in
+	       (Environ.push_named (of_tuple (id,new_v,new_t)) env,mkVar id::ctxt)
       )
 	(Environ.rel_context new_env)
 	~init:(env,[])
@@ -398,7 +402,8 @@ let rec pattern_to_term_and_type env typ  = function
       in
       let constructors = Inductiveops.get_constructors env indf in
       let constructor  = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
-      let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
+      let open Context.Rel.Declaration in
+      let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in
       let _,cstl = Inductiveops.dest_ind_family indf in
       let csta = Array.of_list cstl in
       let implicit_args =
@@ -597,9 +602,10 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	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 new_env =
+          let open Context.Named.Declaration in
 	  match n with
 	      Anonymous -> env
-	    | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env
+	    | Name id -> Environ.push_named (of_tuple (id,Some 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
@@ -875,7 +881,7 @@ exception Continue
 *)
 let rec rebuild_cons env nb_args relname args crossed_types depth rt =
   observe (str "rebuilding : " ++ pr_glob_constr rt);
-
+  let open Context.Rel.Declaration in
   match rt with
     | GProd(_,n,k,t,b) ->
 	let not_free_in_t id = not (is_free_in id t) in
@@ -895,7 +901,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			  mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
 			in
 			let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
-			let new_env = Environ.push_rel (n,None,t') env in
+			let new_env = Environ.push_rel (LocalAssum (n,t')) env in
 			let new_b,id_to_exclude =
 			  rebuild_cons new_env
 			    nb_args relname
@@ -926,7 +932,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let subst_b =
 		      if is_in_b then b else  replace_var_by_term id rt b
 		    in
-		    let new_env = Environ.push_rel (n,None,t') env in
+		    let new_env = Environ.push_rel (LocalAssum (n,t')) env in
 		    let new_b,id_to_exclude =
 		      rebuild_cons
 			new_env
@@ -970,9 +976,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			      (fun acc var_as_constr arg ->
 				 if isRel var_as_constr
 				 then
-				   let (na,_,_) =
-				     Environ.lookup_rel (destRel var_as_constr) env
-				   in
+                                   let open Context.Rel.Declaration in
+				   let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in
 				   match na with
 				     | Anonymous -> acc
 				     | Name id' ->
@@ -1010,7 +1015,7 @@ 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
-		      Environ.push_rel (n,None,t') env
+		      Environ.push_rel (LocalAssum (n,t')) env
 		    in
 		    let new_b,id_to_exclude =
 		      rebuild_cons
@@ -1048,7 +1053,7 @@ 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 rt);
 		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-		let new_env = Environ.push_rel (n,None,t') env in
+		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
@@ -1064,7 +1069,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	    | _ ->
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
 		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-		let new_env = Environ.push_rel (n,None,t') env in
+		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
@@ -1085,7 +1090,7 @@ 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 = Environ.push_rel (n,None,t') env in
+		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
@@ -1108,7 +1113,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let t',ctx = Pretyping.understand env evd t in
 	  let evd = Evd.from_ctx ctx in
 	  let type_t' = Typing.unsafe_type_of env evd t' in
-	  let new_env = Environ.push_rel (n,Some t',type_t') env in
+	  let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
 	      nb_args relname
@@ -1132,7 +1137,7 @@ 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 = Environ.push_rel (na,None,t') env in
+	  let new_env = Environ.push_rel (LocalAssum (na,t')) env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
 	      nb_args relname
@@ -1254,12 +1259,13 @@ let do_build_inductive
   let relnames = Array.map mk_rel_id funnames in
   let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in
   (* Construction of the pseudo constructors *)
+  let open Context.Named.Declaration in
   let evd,env =
     Array.fold_right2
       (fun id c (evd,env) ->
        let evd,t = Typing.type_of env evd (mkConstU c) in
        evd,
-       Environ.push_named (id,None,t)
+       Environ.push_named (LocalAssum (id,t))
 			   (* try *)
 			   (*   Typing.e_type_of env evd (mkConstU c) *)
 			   (* with Not_found -> *)
@@ -1298,8 +1304,8 @@ let do_build_inductive
     *)
     let rel_arities = Array.mapi rel_arity funsargs in
     Util.Array.fold_left2 (fun env rel_name rel_ar ->
-			     Environ.push_named (rel_name,None, 
-						 fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)) env) env relnames rel_arities
+			     Environ.push_named (LocalAssum (rel_name,
+						             fst (with_full_print (Constrintern.interp_constr env evd) rel_ar))) 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 d1e109825..86abf9e2e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,3 +1,4 @@
+open Context.Rel.Declaration
 open Errors
 open Util
 open Names
@@ -13,10 +14,10 @@ open Decl_kinds
 open Sigma.Notations
 
 let is_rec_info scheme_info =
-  let test_branche min acc (_,_,br) =
+  let test_branche min acc decl =
     acc || (
       let new_branche =
-	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in
+	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in
       let free_rels_in_br = Termops.free_rels new_branche in
       let max = min + scheme_info.Tactics.npredicates in
       Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br
@@ -153,7 +154,8 @@ let build_newrecursive
 	let evdref = ref (Evd.from_env env0) in
 	let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
-        (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
+        let open Context.Named.Declaration in
+        (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0c9d3bb81..56bc4328d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -5,6 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+
 open Tacexpr
 open Declarations
 open Errors
@@ -20,6 +21,7 @@ open Indfun_common
 open Tacmach
 open Misctypes
 open Termops
+open Context.Rel.Declaration
 
 (* Some pretty printing function for debugging purpose *)
 
@@ -134,18 +136,21 @@ let generate_type evd g_to_f f graph i =
   let fun_ctxt,res_type =
     match ctxt with
       | [] | [_] -> anomaly (Pp.str "Not a valid context")
-      | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type
+      | decl :: fun_ctxt -> fun_ctxt, get_type decl
   in
   let rec args_from_decl i accu = function
   | [] -> accu
-  | (_, Some _, _) :: l ->
+  | LocalDef _ :: l ->
     args_from_decl (succ i) accu l
   | _ :: l ->
     let t = mkRel i in
     args_from_decl (succ i) (t :: accu) l
   in
   (*i We need to name the vars [res] and [fv] i*)
-  let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in
+  let filter = fun decl -> match get_name decl with
+			   | Name id -> Some id
+			   | Anonymous -> None
+  in
   let named_ctxt = List.map_filter filter fun_ctxt in
   let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in
   let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in
@@ -171,12 +176,12 @@ 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 =
-    (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(f,args_as_rels)),res_type)::fun_ctxt
+    LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, 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 (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
-  else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
+  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
 
 
 (*
@@ -260,10 +265,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     (* and built the intro pattern for each of them *)
     let intro_pats =
       List.map
-	(fun (_,_,br_type) ->
+	(fun decl ->
 	   List.map
 	     (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
-	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
+	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl)))))
 	)
 	branches
     in
@@ -390,10 +395,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	(fun ((_,(ctxt,concl))) ->
 	   match ctxt with
 	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
-	     | hres::res::(x,_,t)::ctxt ->
+	     | hres::res::decl::ctxt ->
 		let res = Termops.it_mkLambda_or_LetIn
 			    (Termops.it_mkProd_or_LetIn concl [hres;res])
-			    ((x,None,t)::ctxt)
+			    (LocalAssum (get_name decl, get_type decl) :: ctxt)
 		in
 		res
 	)
@@ -408,8 +413,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     let bindings =
       let params_bindings,avoid =
 	List.fold_left2
-	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
+	  (fun (bindings,avoid) decl p ->
+	     let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in
 	     p::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
@@ -418,8 +423,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       in
       let lemmas_bindings =
 	List.rev (fst  (List.fold_left2
-	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
+	  (fun (bindings,avoid) decl p ->
+	     let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in
 	     (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
@@ -455,9 +460,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
    generalize every hypothesis which depends of [x] but [hyp]
 *)
 let generalize_dependent_of x hyp g =
+  let open Context.Named.Declaration in
   tclMAP
     (function
-       | (id,None,t) when not (Id.equal id hyp) &&
+       | LocalAssum (id,t) when not (Id.equal id hyp) &&
 	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id])
        | _ -> tclIDTAC
     )
@@ -663,10 +669,10 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let branches = List.rev princ_infos.branches in
     let intro_pats =
       List.map
-	(fun (_,_,br_type) ->
+	(fun decl ->
 	   List.map
 	     (fun id -> id)
-	     (generate_fresh_id (Id.of_string "y") ids (nb_prod br_type))
+	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl)))
 	)
 	branches
     in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 57782dd71..c71d9a9ca 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -24,6 +24,7 @@ open Declarations
 open Glob_term
 open Glob_termops
 open Decl_kinds
+open Context.Rel.Declaration
 
 (** {1 Utilities}  *)
 
@@ -134,9 +135,9 @@ let showind (id:Id.t) =
   let cstrid = Constrintern.global_reference id in
   let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
   let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
-  List.iter (fun (nm, optcstr, tp) ->
-    print_string (string_of_name nm^":");
-    prconstr tp; print_string "\n")
+  List.iter (fun decl ->
+    print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
+    prconstr (get_type decl); print_string "\n")
     ib1.mind_arity_ctxt;
     Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1);
   Array.iteri
@@ -459,11 +460,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
   let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
   let _ = prstr "\notherprms1:\n" in
   let _ =
-    List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n")
+    List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : ");
+			   prconstr (get_type decl); prstr "\n")
     otherprms1 in
   let _ = prstr "\notherprms2:\n" in
   let _ =
-    List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n")
+    List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n")
     otherprms2 in
   {
     ident=id;
@@ -823,9 +825,11 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
   let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
   let arity,_ =
     List.fold_left
-      (fun (acc,env) (nm,_,c) ->
+      (fun (acc,env) decl ->
+        let nm = Context.Rel.Declaration.get_name decl in
+        let c = get_type decl in
         let typ = Constrextern.extern_constr false env Evd.empty c in
-        let newenv = Environ.push_rel (nm,None,c) env in
+        let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
         CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
       (shift.funresprms2 @ shift.funresprms1
@@ -852,10 +856,10 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
 
 let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
   match rdecl with
-    | (nme,None,t) ->
+    | LocalAssum (nme,t) ->
         let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
         GProd (Loc.ghost,nme,Explicit,traw,t2)
-    | (_,Some _,_) -> assert false
+    | LocalDef _ -> assert false
 
 
 (** [merge_inductive ind1 ind2 lnk] merges two graphs, linking
@@ -969,7 +973,7 @@ let funify_branches relinfo nfuns branch =
       | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
       | _ -> false in
   (* FIXME: *)
-  (Anonymous,Some mkProp,mkProp)
+  LocalDef (Anonymous,mkProp,mkProp)
 
 
 let relprinctype_to_funprinctype relprinctype nfuns =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b09678341..09c5aa567 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -40,7 +40,7 @@ open Eauto
 
 open Indfun_common
 open Sigma.Notations
-
+open Context.Rel.Declaration
 
 
 (* Ugly things which should not be here *)
@@ -181,7 +181,7 @@ let (value_f:constr list -> global_reference -> constr) =
       )
     in
     let context = List.map
-      (fun (x, c) -> Name x, None, c) (List.combine rev_x_id_l (List.rev al))
+      (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al))
     in
     let env = Environ.push_rel_context context (Global.env ()) in
     let glob_body =
@@ -678,8 +678,10 @@ let mkDestructEq :
   let hyps = pf_hyps g in
   let to_revert =
     Util.List.map_filter
-      (fun (id, _, t) ->
-        if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t)
+      (fun decl ->
+        let open Context.Named.Declaration in
+        let id = get_id decl in
+        if Id.List.mem id not_on_hyp || not (Termops.occur_term expr (get_type decl))
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
   let type_of_expr = pf_unsafe_type_of g expr in
@@ -1253,7 +1255,7 @@ let clear_goals =
 	  then Termops.pop b'
 	  else if b' == b then t
 	  else mkProd(na,t',b')
-      | _ -> map_constr clear_goal t
+      | _ -> Term.map_constr clear_goal t
   in
   List.map clear_goal
 
@@ -1489,7 +1491,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let env = Global.env() in
   let evd = ref (Evd.from_env env) in
   let function_type = interp_type_evars env evd type_of_f in
-  let env = push_named (function_name,None,function_type) env in
+  let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
   let ty = interp_type_evars env evd ~impls:rec_impls eq in
   let evm, nf = Evarutil.nf_evars_and_universes !evd in
@@ -1497,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let function_type = nf function_type in
  (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
-  let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
+  let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
   let eq' = nf_zeta env_eq' eq'  in
   let res =
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
@@ -1515,7 +1517,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
-  let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
+  let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
   let relation =
     fst (*FIXME*)(interp_constr
       env_with_pre_rec_args
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 7e38109d6..b740649e9 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -28,6 +28,7 @@ open Nametab
 open Contradiction
 open Misctypes
 open Proofview.Notations
+open Context.Named.Declaration
 
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -1695,25 +1696,26 @@ let destructure_hyps =
   let pf_nf = Tacmach.New.of_old pf_nf gl in
     let rec loop = function
       | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
-      | (i,body,t)::lit ->
+      | decl::lit ->
+          let (i,_,t) = to_tuple decl in
 	  begin try match destructurate_prop t with
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
           | Kapp(Or,[t1;t2]) ->
               (Tacticals.New.tclTHENS
                  (elim_id i)
-                 [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
-                   onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
+                 [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit)));
+                   onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ])
           | Kapp(And,[t1;t2]) ->
               Tacticals.New.tclTHEN
 		(elim_id i)
 		(onClearedName2 i (fun i1 i2 ->
-		  loop ((i1,None,t1)::(i2,None,t2)::lit)))
+		  loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit)))
           | Kapp(Iff,[t1;t2]) ->
 	      Tacticals.New.tclTHEN
 		(elim_id i)
 		(onClearedName2 i (fun i1 i2 ->
-		  loop ((i1,None,mkArrow t1 t2)::(i2,None,mkArrow t2 t1)::lit)))
+		  loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit)))
           | Kimp(t1,t2) ->
 	      (* t1 and t2 might be in Type rather than Prop.
 		 For t1, the decidability check will ensure being Prop. *)
@@ -1724,7 +1726,7 @@ let destructure_hyps =
 		  Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp,
                                                                [| t1; t2; d1; mkVar i|])]);
 		  (onClearedName i (fun i ->
-		    (loop ((i,None,mk_or (mk_not t1) t2)::lit))))
+		    (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit))))
                 ]
               else
 		loop lit
@@ -1735,7 +1737,7 @@ let destructure_hyps =
 		    Proofview.V82.tactic (generalize_tac
                                             [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
 		    (onClearedName i (fun i ->
-                      (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
+                      (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit))))
                   ]
 	      | Kapp(And,[t1;t2]) ->
 		  let d1 = decidability t1 in
@@ -1744,7 +1746,7 @@ let destructure_hyps =
 		                            [mkApp (Lazy.force coq_not_and,
 				                    [| t1; t2; d1; mkVar i |])]);
 		    (onClearedName i (fun i ->
-                      (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
+                      (loop (LocalAssum (i,mk_or (mk_not t1) (mk_not t2)) :: lit))))
                   ]
 	      | Kapp(Iff,[t1;t2]) ->
 		  let d1 = decidability t1 in
@@ -1754,9 +1756,8 @@ let destructure_hyps =
 		                            [mkApp (Lazy.force coq_not_iff,
 				                    [| t1; t2; d1; d2; mkVar i |])]);
 		    (onClearedName i (fun i ->
-                      (loop ((i,None,
-			      mk_or (mk_and t1 (mk_not t2))
-				(mk_and (mk_not t1) t2))::lit))))
+                      (loop (LocalAssum (i, mk_or (mk_and t1 (mk_not t2))
+				                  (mk_and (mk_not t1) t2)) :: lit))))
                   ]
 	      | Kimp(t1,t2) ->
 		    (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
@@ -1767,14 +1768,14 @@ let destructure_hyps =
 		                            [mkApp (Lazy.force coq_not_imp,
 				                    [| t1; t2; d1; mkVar i |])]);
 		    (onClearedName i (fun i ->
-                      (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
+                      (loop (LocalAssum (i,mk_and t1 (mk_not t2)) :: lit))))
                   ]
 	      | Kapp(Not,[t]) ->
 		  let d = decidability t in
                   Tacticals.New.tclTHENLIST [
 		    Proofview.V82.tactic (generalize_tac
 			                    [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
-		    (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
+		    (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit))))
                   ]
 	      | Kapp(op,[t1;t2]) ->
 		  (try
@@ -1807,15 +1808,13 @@ let destructure_hyps =
 		    match destructurate_type (pf_nf typ) with
 		    | Kapp(Nat,_) ->
                         (Tacticals.New.tclTHEN
-			   (convert_hyp_no_check
-                                                    (i,body,
-				                     (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
+			   (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
+                                                           decl))
 			   (loop lit))
 		    | Kapp(Z,_) ->
                         (Tacticals.New.tclTHEN
-			   (convert_hyp_no_check
-                                                    (i,body,
-				                     (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
+			   (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
+                                                           decl))
 			   (loop lit))
 		    | _ -> loop lit
                   end
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 9c22b5adb..2f3a3e551 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -13,6 +13,7 @@ open Util
 open Term
 open Tacmach
 open Proof_search
+open Context.Named.Declaration
 
 let force count lazc = incr count;Lazy.force lazc
 
@@ -128,9 +129,9 @@ let rec make_form atom_env gls term =
 
 let rec make_hyps atom_env gls lenv = function
     [] -> []
-  | (_,Some body,typ)::rest ->
+  | LocalDef (_,body,typ)::rest ->
       make_hyps atom_env gls (typ::body::lenv) rest
-  | (id,None,typ)::rest ->
+  | LocalAssum (id,typ)::rest ->
       let hrec=
 	make_hyps atom_env gls (typ::lenv) rest in
 	if List.exists (Termops.dependent (mkVar id)) lenv ||
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index c9e591bbd..9a14ac6c7 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -18,7 +18,7 @@ val make_hyps :
     atom_env ->
     Proof_type.goal Tacmach.sigma ->
     Term.types list ->
-    (Names.Id.t * Term.types option * Term.types) list ->
+    Context.Named.t ->
     (Names.Id.t * Proof_search.form) list
 
 val rtauto_tac : Proof_type.tactic