2 files changed, 5 insertions, 4 deletions
diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v
index d1cb802755..342c03dbac 100644
--- a/contrib/rtauto/Rtauto.v
+++ b/contrib/rtauto/Rtauto.v
@@ -18,7 +18,7 @@ Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
 Ltac clean:=try (simpl;congruence).
 
 Inductive form:Set:=
-Atom : positive -> form
+  Atom : positive -> form
 | Arrow : form -> form -> form
 | Bot
 | Conjunct : form -> form -> form 
@@ -395,4 +395,4 @@ exact (Reflect (empty \ A \ B \ C)
   (I_Or_r (I_And (Ax 2) (Ax 4))))))).
 Qed.
 Print toto.
-*)
-\ No newline at end of file
+*)
diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml
index 0865a825c9..801122476e 100644
--- a/contrib/rtauto/refl_tauto.ml
+++ b/contrib/rtauto/refl_tauto.ml
@@ -113,7 +113,7 @@ let rec make_form atom_env gls term =
 	      Arrow (fa,fb)
 	  else
 	    make_atom atom_env (normalize term)
-      | Cast(a,b) -> 
+      | Cast(a,_,_) -> 
 	  make_form atom_env gls a
       | Ind ind ->
 	  if ind = Lazy.force li_False then
@@ -273,7 +273,8 @@ let rtauto_tac gls=
       (pf_env gls) (Tacmach.project gls) gl <> InProp 
     then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
   let glf=make_form gamma gls gl in
-  let hyps=make_hyps gamma gls [gl] gls.it.evar_hyps in
+  let hyps=make_hyps gamma gls [gl] 
+      (Environ.named_context_of_val gls.it.evar_hyps) in
   let formula=
     List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in  
   let search_fun =