Add relevance marks on binders.

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

4 files changed, 11 insertions, 9 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 797b6faa08..8bf86e9ef6 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -505,9 +505,9 @@ let gallina_print_named_decl env sigma =
   let open Context.Named.Declaration in
   function
   | LocalAssum (id, typ) ->
-     print_named_assum env sigma (Id.to_string id) typ
+     print_named_assum env sigma (Id.to_string id.Context.binder_name) typ
   | LocalDef (id, body, typ) ->
-     print_named_def env sigma (Id.to_string id) body typ
+     print_named_def env sigma (Id.to_string id.Context.binder_name) body typ
 
 let assumptions_for_print lna =
   List.fold_right (fun na env -> add_name na env) lna empty_names_context
diff --git a/printing/printer.ml b/printing/printer.ml
index bc936975c2..fa55a28cb3 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -13,6 +13,7 @@ open CErrors
 open Util
 open Names
 open Constr
+open Context
 open Environ
 open Globnames
 open Evd
@@ -100,7 +101,7 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
   (* Warning: clashes can occur with variables of same name in env but *)
   (* we also need to preserve the actual names of the patterns *)
   (* So what to do? *)
-  let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
+  let assums = List.map (fun id -> (make_annot (Name id) Sorts.Relevant,(* dummy *) mkProp)) ids in
   pr (Termops.push_rels_assum assums env) sigma c
 
 let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env
@@ -290,7 +291,7 @@ let pr_compacted_decl env sigma decl =
        let pb = if isCast c then surround pb else pb in
        ids, (str" := " ++ pb ++ cut ()), typ
   in
-  let pids = prlist_with_sep pr_comma pr_id ids in
+  let pids = prlist_with_sep pr_comma (fun id -> pr_id id.binder_name) ids in
   let pt = pr_ltype_env env sigma typ in
   let ptyp = (str" : " ++ pt) in
   hov 0 (pids ++ pbody ++ ptyp)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 3438063f76..f4986652b3 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -10,6 +10,7 @@
 
 open Util
 open Constr
+open Context
 open Pp
 open Names
 open Environ
@@ -132,10 +133,10 @@ let get_fields =
   let rec prodec_rec l subst c =
     match kind c with
     | Prod (na,t,c) ->
-        let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
+        let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in
         prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c
     | LetIn (na,b,_,c) ->
-        let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
+        let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in
         prodec_rec ((id,false,Vars.substl subst b)::l) (mkVar id::subst) c
     | _               -> List.rev l
   in
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 878e9f477b..5aa7b3c7bd 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -204,14 +204,14 @@ let diff_hyps o_line_idents o_map n_line_idents n_map =
   List.rev !rv;;
 
 
-type 'a hyp = (Names.Id.t list * 'a option * 'a)
+type 'a hyp = (Names.Id.t Context.binder_annot list * 'a option * 'a)
 type 'a reified_goal = { name: string; ty: 'a; hyps: 'a hyp list; env : Environ.env; sigma: Evd.evar_map }
 
 (* XXX: Port to proofview, one day. *)
 (* open Proofview *)
 module CDC = Context.Compacted.Declaration
 
-let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * 'pc) =
+let to_tuple : Constr.compacted_declaration -> (Names.Id.t Context.binder_annot list * 'pc option * 'pc) =
   let open CDC in function
     | LocalAssum(idl, tm)   -> (idl, None, EConstr.of_constr tm)
     | LocalDef(idl,tdef,tm) -> (idl, Some (EConstr.of_constr tdef), EConstr.of_constr tm);;
@@ -283,7 +283,7 @@ let goal_info goal sigma =
   let build_hyp_info env sigma hyp =
     let (names, body, ty) = hyp in
     let open Pp in
-    let idents = List.map (fun x -> Names.Id.to_string x) names in
+    let idents = List.map (fun x -> Names.Id.to_string x.Context.binder_name) names in
 
     line_idents := idents :: !line_idents;
     let mid = match body with