3 files changed, 7 insertions, 7 deletions
diff --git a/contrib/ring/g_quote.ml4 b/contrib/ring/g_quote.ml4
index e439feb8c..808cbbf27 100644
--- a/contrib/ring/g_quote.ml4
+++ b/contrib/ring/g_quote.ml4
@@ -12,7 +12,7 @@
 
 open Quote
 
-TACTIC EXTEND Quote
-  [ "Quote" ident(f) ] -> [ quote f [] ]
-| [ "Quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
+TACTIC EXTEND quote
+  [ "quote" ident(f) ] -> [ quote f [] ]
+| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
 END
diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4
index 9c0e5c4e7..0cb86dfdd 100644
--- a/contrib/ring/g_ring.ml4
+++ b/contrib/ring/g_ring.ml4
@@ -13,8 +13,8 @@
 open Quote
 open Ring
 
-TACTIC EXTEND Ring
-  [ "Ring" constr_list(l) ] -> [ polynom l ]
+TACTIC EXTEND ring
+  [ "ring" constr_list(l) ] -> [ polynom l ]
 END
 
 (* The vernac commands "Add Ring" and co *)
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 4884f23c6..5448d1389 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -835,11 +835,11 @@ let raw_polynom th op lc gl =
            (tclORELSE
               (tclORELSE
 		 (h_exact c'i_eq_c''i)
-		 (h_exact (mkApp(build_coq_sym_eqT (),
+		 (h_exact (mkApp(build_coq_sym_eq (),
 				 [|th.th_a; c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS 
 		 (elim_type 
-		    (mkApp(build_coq_eqT (), [|th.th_a; c'''i; ci |])))
+		    (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |])))
 		 [ tac;
                    h_exact c'i_eq_c''i ]))
 )