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.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/rtauto/refl_tauto.mli')

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