3 files changed, 4 insertions, 6 deletions
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 776ebd808d..14aead0452 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -263,7 +263,7 @@ Section ALMOST_RING.
  Variable SRth : semi_ring_theory 0 1 radd rmul req.
 
  (** Every semi ring can be seen as an almost ring, by taking :
-        -x = x and x - y = x + y *)
+        [-x = x] and [x - y = x + y] *)
  Definition SRopp (x:R) := x. Notation "- x" := (SRopp x).
 
  Definition SRsub x y := x + -y. Infix "-" := SRsub.
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index a7d6d5bb20..b34d12952f 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Ltac_plugin
 open Pp
 open Util
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e3e749b754..125afb1a0e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -166,12 +166,12 @@ let ltac_call tac (args:glob_tactic_arg list) =
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar(Loc.tag @@ Id.of_string tac),args)))
+  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args)))
 
 let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
   let fold arg (i, vars, lfun) =
     let id = Id.of_string ("x" ^ string_of_int i) in
-    let x = Reference (ArgVar (Loc.tag id)) in
+    let x = Reference (ArgVar CAst.(make id)) in
     (succ i, x :: vars, Id.Map.add id arg lfun)
   in
   let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
@@ -206,7 +206,7 @@ let get_res =
 let exec_tactic env evd n f args =
   let fold arg (i, vars, lfun) =
     let id = Id.of_string ("x" ^ string_of_int i) in
-    let x = Reference (ArgVar (Loc.tag id)) in
+    let x = Reference (ArgVar CAst.(make id)) in
     (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun)
   in
   let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in