3 files changed, 8 insertions, 7 deletions
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 751f0d8334..c2dec264ad 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -294,10 +294,10 @@ Qed.
 
 End Store.
 
-Arguments PNone [A].
+Arguments PNone {A}.
 Arguments PSome [A] _.
 
-Arguments Tempty [A].
+Arguments Tempty {A}.
 Arguments Branch0 [A] _ _.
 Arguments Branch1 [A] _ _ _.
 
@@ -311,7 +311,7 @@ Arguments mkStore [A] index contents.
 Arguments index [A] s.
 Arguments contents [A] s.
 
-Arguments empty [A].
+Arguments empty {A}.
 Arguments get [A] i S.
 Arguments push [A] a S.
 
@@ -319,7 +319,7 @@ Arguments get_empty [A] i.
 Arguments get_push_Full [A] i a S _.
 
 Arguments Full [A] _.
-Arguments F_empty [A].
+Arguments F_empty {A}.
 Arguments F_push [A] a S _.
 Arguments In [A] x S F.
 
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