From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 plugins/rtauto/refl_tauto.ml  | 5 +++--
 plugins/rtauto/refl_tauto.mli | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index a6b6c57ff9..89528fe357 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -16,6 +16,7 @@ open CErrors
 open Util
 open Term
 open Constr
+open Context
 open Proof_search
 open Context.Named.Declaration
 
@@ -127,7 +128,7 @@ let rec make_hyps env sigma atom_env lenv = function
   | LocalAssum (id,typ)::rest ->
     let hrec=
       make_hyps env sigma atom_env (typ::lenv) rest in
-    if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv ||
+    if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id.binder_name c) lenv ||
        (Retyping.get_sort_family_of env sigma typ != InProp)
     then
       hrec
@@ -291,7 +292,7 @@ let rtauto_tac =
                         build_form formula;
                         build_proof [] 0 prf|]) in
     let term=
-      applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in
+      applistc main (List.rev_map (fun (id,_) -> mkVar id.binder_name) hyps) in
     let build_end_time=System.get_time () in
     let () = if !verbose then
         begin
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 49b5ee5ac7..3de0ba44df 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -23,6 +23,6 @@ val make_hyps
   -> atom_env
   -> EConstr.types list
   -> EConstr.named_context
-  -> (Names.Id.t * Proof_search.form) list
+  -> (Names.Id.t Context.binder_annot * Proof_search.form) list
 
 val rtauto_tac : unit Proofview.tactic
-- 
cgit v1.2.3