{new,setoid_}ring -> ring

I believe this renaming makes it easier for new contributors to discover
the code of `ring`.

7 files changed, 1319 insertions, 0 deletions

diff --git a/plugins/ring/dune b/plugins/ring/dune
new file mode 100644
index 0000000000..080d8c672e
--- /dev/null
+++ b/plugins/ring/dune
@@ -0,0 +1,7 @@
+(library
+ (name ring_plugin)
+ (public_name coq.plugins.ring)
+ (synopsis "Coq's ring plugin")
+ (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_ring))
diff --git a/plugins/ring/g_ring.mlg b/plugins/ring/g_ring.mlg
new file mode 100644
index 0000000000..3c800987ac
--- /dev/null
+++ b/plugins/ring/g_ring.mlg
@@ -0,0 +1,133 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+{
+
+open Ltac_plugin
+open Pp
+open Util
+open Ring_ast
+open Ring
+open Stdarg
+open Tacarg
+open Pcoq.Constr
+open Pltac
+
+}
+
+DECLARE PLUGIN "ring_plugin"
+
+TACTIC EXTEND protect_fv
+| [ "protect_fv" string(map) "in" ident(id) ] ->
+    { protect_tac_in map id }
+| [ "protect_fv" string(map) ] ->
+    { protect_tac map }
+END
+
+{
+
+open Pptactic
+open Ppconstr
+
+let pr_ring_mod env sigma = function
+  | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg (pr_constr_expr env sigma) eq_test
+  | Ring_kind Abstract ->  str "abstract"
+  | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg (pr_constr_expr env sigma) morph
+  | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
+  | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
+  | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
+  | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
+  | Setoid(sth,ext) -> str "setoid" ++ pr_arg (pr_constr_expr env sigma) sth ++ pr_arg (pr_constr_expr env sigma) ext
+  | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
+  | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
+  | Sign_spec t -> str "sign" ++ pr_arg (pr_constr_expr env sigma) t
+  | Div_spec t -> str "div" ++ pr_arg (pr_constr_expr env sigma) t
+
+}
+
+VERNAC ARGUMENT EXTEND ring_mod
+  PRINTED BY { pr_ring_mod env sigma }
+  | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) }
+  | [ "abstract" ] -> { Ring_kind Abstract }
+  | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) }
+  | [ "constants" "[" tactic(cst_tac) "]" ] -> { Const_tac(CstTac cst_tac) }
+  | [ "closed" "[" ne_global_list(l) "]" ] -> { Const_tac(Closed l) }
+  | [ "preprocess" "[" tactic(pre) "]" ] -> { Pre_tac pre }
+  | [ "postprocess" "[" tactic(post) "]" ] -> { Post_tac post }
+  | [ "setoid" constr(sth) constr(ext) ] -> { Setoid(sth,ext) }
+  | [ "sign" constr(sign_spec) ] -> { Sign_spec sign_spec }
+  | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] ->
+           { Pow_spec (Closed l, pow_spec) }
+  | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] ->
+           { Pow_spec (CstTac cst_tac, pow_spec) }
+  | [ "div" constr(div_spec) ] -> { Div_spec div_spec }
+END
+
+{
+
+let pr_ring_mods env sigma l = surround (prlist_with_sep pr_comma (pr_ring_mod env sigma) l)
+
+}
+
+VERNAC ARGUMENT EXTEND ring_mods
+  PRINTED BY { pr_ring_mods env sigma }
+  | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods }
+END
+
+VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
+  | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] ->
+    { add_theory id t (Option.default [] l) }
+  | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> {
+    print_rings ()
+  }
+END
+
+TACTIC EXTEND ring_lookup
+| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
+    { let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t }
+END
+
+{
+
+let pr_field_mod env sigma = function
+  | Ring_mod m -> pr_ring_mod env sigma m
+  | Inject inj -> str "completeness" ++ pr_arg (pr_constr_expr env sigma) inj
+
+}
+
+VERNAC ARGUMENT EXTEND field_mod
+  PRINTED BY { pr_field_mod env sigma }
+  | [ ring_mod(m) ] -> { Ring_mod m }
+  | [ "completeness" constr(inj) ] -> { Inject inj }
+END
+
+{
+
+let pr_field_mods env sigma l = surround (prlist_with_sep pr_comma (pr_field_mod env sigma) l)
+
+}
+
+VERNAC ARGUMENT EXTEND field_mods
+  PRINTED BY { pr_field_mods env sigma }
+  | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods }
+END
+
+VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
+| [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] ->
+  { let l = match l with None -> [] | Some l -> l in add_field_theory id t l }
+| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> {
+    print_fields ()
+  }
+END
+
+TACTIC EXTEND field_lookup
+| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
+      { let (t,l) = List.sep_last lt in field_lookup f lH l t }
+END
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
new file mode 100644
index 0000000000..9c75175889
--- /dev/null
+++ b/plugins/ring/ring.ml
@@ -0,0 +1,996 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+module CVars = Vars
+open Ltac_plugin
+open Pp
+open Util
+open Names
+open Constr
+open EConstr
+open Vars
+open CClosure
+open Environ
+open Glob_term
+open Locus
+open Tacexpr
+open Coqlib
+open Mod_subst
+open Tacinterp
+open Libobject
+open Printer
+open Declare
+open Entries
+open Ring_ast
+open Proofview.Notations
+
+let error msg = CErrors.user_err Pp.(str msg)
+
+(****************************************************************************)
+(* controlled reduction *)
+
+type protect_flag = Eval|Prot|Rec
+
+type protection = Evd.evar_map -> EConstr.t -> GlobRef.t -> (Int.t -> protect_flag) option
+
+let global_head_of_constr sigma c =
+  let f, args = decompose_app sigma c in
+    try fst (EConstr.destRef sigma f)
+    with DestKO -> CErrors.anomaly (str "global_head_of_constr.")
+
+let global_of_constr_nofail c =
+  try fst @@ Constr.destRef c
+  with DestKO -> GlobRef.VarRef (Id.of_string "dummy")
+
+let rec mk_clos_but f_map n t =
+  let (f, args) = Constr.decompose_appvect t in
+  match f_map (global_of_constr_nofail f) with
+  | Some tag ->
+      let map i t = tag_arg f_map n (tag i) t in
+      if Array.is_empty args then map (-1) f
+      else mk_red (FApp (map (-1) f, Array.mapi map args))
+  | None -> mk_atom t
+
+and tag_arg f_map n tag c = match tag with
+| Eval -> mk_clos (Esubst.subs_id n) c
+| Prot -> mk_atom c
+| Rec -> mk_clos_but f_map n c
+
+let interp_map l t =
+  try Some(List.assoc_f GlobRef.equal t l) with Not_found -> None
+
+let protect_maps : protection String.Map.t ref = ref String.Map.empty
+let add_map s m = protect_maps := String.Map.add s m !protect_maps
+let lookup_map map =
+  try String.Map.find map !protect_maps
+  with Not_found ->
+    CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
+
+let protect_red map env sigma c0 =
+  let evars ev = Evarutil.safe_evar_value sigma ev in
+  let c = EConstr.Unsafe.to_constr c0 in
+  let tab = create_tab () in
+  let infos = create_clos_infos ~univs:(Evd.universes sigma) ~evars all env in
+  let map = lookup_map map sigma c0 in
+  let rec eval n c = match Constr.kind c with
+  | Prod (na, t, u) -> Constr.mkProd (na, eval n t, eval (n + 1) u)
+  | _ -> kl infos tab (mk_clos_but map n c)
+  in
+  EConstr.of_constr (eval 0 c)
+
+let protect_tac map =
+  Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) None
+
+let protect_tac_in map id =
+  Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))
+
+
+(****************************************************************************)
+
+let rec closed_under sigma cset t =
+  try
+    let (gr, _) = destRef sigma t in
+    GlobRef.Set_env.mem gr cset
+  with DestKO ->
+    match EConstr.kind sigma t with
+    | Cast(c,_,_) -> closed_under sigma cset c
+    | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l
+    | _ -> false
+
+let closed_term args _ = match args with
+| [t; l] ->
+  let t = Option.get (Value.to_constr t) in
+  let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let cs = List.fold_right GlobRef.Set_env.add l GlobRef.Set_env.empty in
+  if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
+| _ -> assert false
+
+let closed_term_ast =
+  let tacname = {
+    mltac_plugin = "ring_plugin";
+    mltac_tactic = "closed_term";
+  } in
+  let () = Tacenv.register_ml_tactic tacname [|closed_term|] in
+  let tacname = {
+    mltac_name = tacname;
+    mltac_index = 0;
+  } in
+  fun l ->
+  let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
+  TacFun([Name(Id.of_string"t")],
+  TacML(CAst.make (tacname,
+  [TacGeneric (None, Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None));
+   TacGeneric (None, Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
+(*
+let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
+*)
+
+(****************************************************************************)
+
+let ic c =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  let c, uctx = Constrintern.interp_constr env sigma c in
+  (Evd.from_ctx uctx, c)
+
+let ic_unsafe c = (*FIXME remove *)
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  fst (Constrintern.interp_constr env sigma c)
+
+let decl_constant name univs c =
+  let open Constr in
+  let vars = CVars.universes_of_constr c in
+  let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in
+  let () = DeclareUctx.declare_universe_context ~poly:false univs in
+  let types = (Typeops.infer (Global.env ()) c).uj_type in
+  let univs = Monomorphic_entry Univ.ContextSet.empty in
+  mkConst(declare_constant ~name
+            ~kind:Decls.(IsProof Lemma)
+            (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c)))
+
+let decl_constant na suff univs c =
+  let na = Namegen.next_global_ident_away (Nameops.add_suffix na suff) Id.Set.empty in
+  decl_constant na univs c
+
+(* Calling a global tactic *)
+let ltac_call tac (args:glob_tactic_arg list) =
+  TacArg(CAst.make @@ TacCall (CAst.make (ArgArg(Loc.tag @@ Lazy.force tac),args)))
+
+let dummy_goal env sigma =
+  let (gl,_,sigma) =
+    Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in
+  {Evd.it = gl; Evd.sigma = sigma}
+
+let constr_of evd v = match Value.to_constr v with
+  | Some c -> EConstr.to_constr evd c
+  | None -> failwith "Ring.exec_tactic: anomaly"
+
+let tactic_res = ref [||]
+
+let get_res =
+  let open Tacexpr in
+  let name = { mltac_plugin = "ring_plugin"; mltac_tactic = "get_res"; } in
+  let entry = { mltac_name = name; mltac_index = 0 } in
+  let tac args ist =
+    let n = Tacinterp.Value.cast (Genarg.topwit Stdarg.wit_int) (List.hd args) in
+    let init i = Id.Map.find (Id.of_string ("x" ^ string_of_int i)) ist.lfun in
+    tactic_res := Array.init n init;
+    Proofview.tclUNIT ()
+  in
+  Tacenv.register_ml_tactic name [| tac |];
+  entry
+
+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 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
+  let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
+  (* Build the getter *)
+  let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
+  let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
+  let get_res = TacML (CAst.make (get_res, [TacGeneric (None, n)])) in
+  let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
+  (* Evaluate the whole result *)
+  let gl = dummy_goal env evd in
+  let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
+  let evd = Evd.minimize_universes gls.Evd.sigma in
+  let nf c = constr_of evd c in
+  Array.map nf !tactic_res, Evd.universe_context_set evd
+
+let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)))
+let gen_reference n = lazy (Coqlib.lib_ref n)
+
+let coq_mk_Setoid = gen_constant "plugins.ring.Build_Setoid_Theory"
+let coq_None = gen_reference "core.option.None"
+let coq_Some = gen_reference "core.option.Some"
+let coq_eq = gen_constant "core.eq.type"
+
+let coq_cons = gen_reference "core.list.cons"
+let coq_nil = gen_reference "core.list.nil"
+
+let lapp f args = mkApp(Lazy.force f,args)
+
+let plapp evdref f args =
+  let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in
+  evdref := evd;
+  mkApp(fc,args)
+
+let dest_rel0 sigma t =
+  match EConstr.kind sigma t with
+  | App(f,args) when Array.length args >= 2 ->
+      let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in
+      if closed0 sigma rel then
+        (rel,args.(Array.length args - 2),args.(Array.length args - 1))
+      else error "ring: cannot find relation (not closed)"
+  | _ -> error "ring: cannot find relation"
+
+let rec dest_rel sigma t =
+  match EConstr.kind sigma t with
+  | Prod(_,_,c) -> dest_rel sigma c
+  | _ -> dest_rel0 sigma t
+
+(****************************************************************************)
+(* Library linking *)
+
+let plugin_dir = "setoid_ring"
+
+let cdir = ["Coq";plugin_dir]
+let plugin_modules =
+  List.map (fun d -> cdir@d)
+    [["Ring_theory"];["Ring_polynom"]; ["Ring_tac"];["InitialRing"];
+     ["Field_tac"]; ["Field_theory"]
+    ]
+
+let my_constant c =
+  lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
+    [@@ocaml.warning "-3"]
+let my_reference c =
+  lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
+    [@@ocaml.warning "-3"]
+
+let znew_ring_path =
+  DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
+let zltac s =
+  lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s))
+
+let mk_cst l s = lazy (Coqlib.coq_reference "ring" l s) [@@ocaml.warning "-3"]
+let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s
+
+(* Ring theory *)
+
+(* almost_ring defs *)
+let coq_almost_ring_theory = my_constant "almost_ring_theory"
+
+(* setoid and morphism utilities *)
+let coq_eq_setoid = my_reference "Eqsth"
+let coq_eq_morph = my_reference "Eq_ext"
+let coq_eq_smorph = my_reference "Eq_s_ext"
+
+(* ring -> almost_ring utilities *)
+let coq_ring_theory = my_constant "ring_theory"
+let coq_mk_reqe = my_constant "mk_reqe"
+
+(* semi_ring -> almost_ring utilities *)
+let coq_semi_ring_theory = my_constant "semi_ring_theory"
+let coq_mk_seqe = my_constant "mk_seqe"
+
+let coq_abstract = my_constant"Abstract"
+let coq_comp = my_constant"Computational"
+let coq_morph = my_constant"Morphism"
+
+(* power function *)
+let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
+
+(* hypothesis *)
+let coq_mkhypo = my_reference "mkhypo"
+let coq_hypo = my_reference "hypo"
+
+(* Equality: do not evaluate but make recursive call on both sides *)
+let map_with_eq arg_map sigma c =
+  let (req,_,_) = dest_rel sigma c in
+  interp_map
+    ((global_head_of_constr sigma req,(function -1->Prot|_->Rec))::
+    List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
+
+let map_without_eq arg_map _ _ =
+  interp_map (List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
+
+let _ = add_map "ring"
+  (map_with_eq
+    [coq_cons,(function -1->Eval|2->Rec|_->Prot);
+    coq_nil, (function -1->Eval|_ -> Prot);
+    my_reference "IDphi", (function _->Eval);
+    my_reference "gen_phiZ", (function _->Eval);
+    (* Pphi_dev: evaluate polynomial and coef operations, protect
+       ring operations and make recursive call on the var map *)
+    pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
+    pol_cst "Pphi_pow",
+          (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
+    (* PEeval: evaluate polynomial, protect ring
+       operations and make recursive call on the var map *)
+    pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot)])
+
+(****************************************************************************)
+(* Ring database *)
+
+module Cmap = Map.Make(Constr)
+
+let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
+
+let print_rings () =
+  Feedback.msg_notice (strbrk "The following ring structures have been declared:");
+  Cmap.iter (fun _carrier ring ->
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
+      Feedback.msg_notice
+        (hov 2
+           (Ppconstr.pr_id ring.ring_name ++ spc() ++
+            str"with carrier "++ pr_constr_env env sigma ring.ring_carrier++spc()++
+            str"and equivalence relation "++ pr_constr_env env sigma ring.ring_req))
+    ) !from_carrier
+
+let ring_for_carrier r = Cmap.find r !from_carrier
+
+let find_ring_structure env sigma l =
+  match l with
+    | t::cl' ->
+        let ty = Retyping.get_type_of env sigma t in
+        let check c =
+          let ty' = Retyping.get_type_of env sigma c in
+          if not (Reductionops.is_conv env sigma ty ty') then
+            CErrors.user_err ~hdr:"ring"
+              (str"arguments of ring_simplify do not have all the same type")
+        in
+        List.iter check cl';
+        (try ring_for_carrier (EConstr.to_constr sigma ty)
+        with Not_found ->
+          CErrors.user_err ~hdr:"ring"
+            (str"cannot find a declared ring structure over"++
+             spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\""))
+    | [] -> assert false
+
+let add_entry e =
+  from_carrier := Cmap.add e.ring_carrier e !from_carrier
+
+let subst_th (subst,th) =
+  let c' = subst_mps subst th.ring_carrier in
+  let eq' = subst_mps subst th.ring_req in
+  let set' = subst_mps subst th.ring_setoid in
+  let ext' = subst_mps subst th.ring_ext in
+  let morph' = subst_mps subst th.ring_morph in
+  let th' = subst_mps subst th.ring_th in
+  let thm1' = subst_mps subst th.ring_lemma1 in
+  let thm2' = subst_mps subst th.ring_lemma2 in
+  let tac'= Tacsubst.subst_tactic subst th.ring_cst_tac in
+  let pow_tac'= Tacsubst.subst_tactic subst th.ring_pow_tac in
+  let pretac'= Tacsubst.subst_tactic subst th.ring_pre_tac in
+  let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in
+  if c' == th.ring_carrier &&
+     eq' == th.ring_req &&
+     Constr.equal set' th.ring_setoid &&
+     ext' == th.ring_ext &&
+     morph' == th.ring_morph &&
+     th' == th.ring_th &&
+     thm1' == th.ring_lemma1 &&
+     thm2' == th.ring_lemma2 &&
+     tac' == th.ring_cst_tac &&
+     pow_tac' == th.ring_pow_tac &&
+     pretac' == th.ring_pre_tac &&
+     posttac' == th.ring_post_tac then th
+  else
+    { ring_name = th.ring_name;
+      ring_carrier = c';
+      ring_req = eq';
+      ring_setoid = set';
+      ring_ext = ext';
+      ring_morph = morph';
+      ring_th = th';
+      ring_cst_tac = tac';
+      ring_pow_tac = pow_tac';
+      ring_lemma1 = thm1';
+      ring_lemma2 = thm2';
+      ring_pre_tac = pretac';
+      ring_post_tac = posttac' }
+
+
+let theory_to_obj : ring_info -> obj =
+  let cache_th (_, th) = add_entry th in
+  declare_object @@ global_object_nodischarge "tactic-new-ring-theory"
+    ~cache:cache_th
+    ~subst:(Some subst_th)
+
+let setoid_of_relation env evd a r =
+  try
+    let evm = !evd in
+    let evm, refl = Rewrite.get_reflexive_proof env evm a r in
+    let evm, sym = Rewrite.get_symmetric_proof env evm a r in
+    let evm, trans = Rewrite.get_transitive_proof env evm a r in
+      evd := evm;
+      lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
+  with Not_found ->
+    error "cannot find setoid relation"
+
+let op_morph r add mul opp req m1 m2 m3 =
+  lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]
+
+let op_smorph r add mul req m1 m2 =
+  lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
+
+let ring_equality env evd (r,add,mul,opp,req) =
+  match EConstr.kind !evd req with
+    | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
+        let setoid = plapp evd coq_eq_setoid [|r|] in
+        let op_morph =
+          match opp with
+              Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
+          | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
+        let sigma = !evd in
+        let sigma, setoid = Typing.solve_evars env sigma setoid in
+        let sigma, op_morph = Typing.solve_evars env sigma op_morph in
+        evd := sigma;
+        (setoid,op_morph)
+    | _ ->
+        let setoid = setoid_of_relation (Global.env ()) evd r req in
+        let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
+        let add_m, add_m_lem =
+          try Rewrite.default_morphism signature add
+          with Not_found ->
+            error "ring addition should be declared as a morphism" in
+        let mul_m, mul_m_lem =
+          try Rewrite.default_morphism signature mul
+          with Not_found ->
+            error "ring multiplication should be declared as a morphism" in
+        let op_morph =
+          match opp with
+            | Some opp ->
+                (let opp_m,opp_m_lem =
+                  try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp
+                  with Not_found ->
+                    error "ring opposite should be declared as a morphism" in
+                let op_morph =
+                  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
+                  Flags.if_verbose
+                    Feedback.msg_info
+                    (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++
+                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
+                        str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++
+                        str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++
+                        str"\"");
+                  op_morph)
+            | None ->
+                (Flags.if_verbose
+                    Feedback.msg_info
+                    (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++
+                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
+                        str"\""++spc()++str"and \""++
+                        pr_econstr_env env !evd mul_m_lem++str"\"");
+                 op_smorph r add mul req add_m_lem mul_m_lem) in
+          (setoid,op_morph)
+
+let build_setoid_params env evd r add mul opp req eqth =
+  match eqth with
+      Some th -> th
+    | None -> ring_equality env evd (r,add,mul,opp,req)
+
+let dest_ring env sigma th_spec =
+  let th_typ = Retyping.get_type_of env sigma th_spec in
+  match EConstr.kind sigma th_typ with
+      App(f,[|r;zero;one;add;mul;sub;opp;req|])
+        when eq_constr_nounivs sigma f (Lazy.force coq_almost_ring_theory) ->
+          (None,r,zero,one,add,mul,Some sub,Some opp,req)
+    | App(f,[|r;zero;one;add;mul;req|])
+        when eq_constr_nounivs sigma f (Lazy.force coq_semi_ring_theory) ->
+        (Some true,r,zero,one,add,mul,None,None,req)
+    | App(f,[|r;zero;one;add;mul;sub;opp;req|])
+        when eq_constr_nounivs sigma f (Lazy.force coq_ring_theory) ->
+        (Some false,r,zero,one,add,mul,Some sub,Some opp,req)
+    | _ -> error "bad ring structure"
+
+
+let reflect_coeff rkind =
+  (* We build an ill-typed terms on purpose... *)
+  match rkind with
+      Abstract -> Lazy.force coq_abstract
+    | Computational c -> lapp coq_comp [|c|]
+    | Morphism m -> lapp coq_morph [|m|]
+
+let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
+  match cst_tac with
+      Some (CstTac t) -> Tacintern.glob_tactic t
+    | Some (Closed lc) ->
+        closed_term_ast (List.map Smartlocate.global_with_alias lc)
+    | None ->
+        let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in
+              TacArg(CAst.make (TacCall(CAst.make (t,[]))))
+
+let make_hyp env evd c =
+  let t = Retyping.get_type_of env !evd c in
+   plapp evd coq_mkhypo [|t;c|]
+
+let make_hyp_list env evdref lH =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
+  let l =
+    List.fold_right
+      (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH
+      (plapp evdref coq_nil [|carrier|])
+  in
+  let sigma, l' = Typing.solve_evars env !evdref l in
+  evdref := sigma;
+  let l' = EConstr.Unsafe.to_constr l' in
+    Evarutil.nf_evars_universes !evdref l'
+
+let interp_power env evdref pow =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
+  match pow with
+  | None ->
+      let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
+      (TacArg(CAst.make (TacCall(CAst.make (t,[])))), plapp evdref coq_None [|carrier|])
+  | Some (tac, spec) ->
+      let tac =
+        match tac with
+        | CstTac t -> Tacintern.glob_tactic t
+        | Closed lc ->
+            closed_term_ast (List.map Smartlocate.global_with_alias lc) in
+      let spec = make_hyp env evdref (ic_unsafe spec) in
+      (tac, plapp evdref coq_Some [|carrier; spec|])
+
+let interp_sign env evdref sign =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
+  match sign with
+  | None -> plapp evdref coq_None [|carrier|]
+  | Some spec ->
+      let spec = make_hyp env evdref (ic_unsafe spec) in
+      plapp evdref coq_Some [|carrier;spec|]
+       (* Same remark on ill-typed terms ... *)
+
+let interp_div env evdref div =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
+  match div with
+  | None -> plapp evdref coq_None [|carrier|]
+  | Some spec ->
+      let spec = make_hyp env evdref (ic_unsafe spec) in
+      plapp evdref coq_Some [|carrier;spec|]
+       (* Same remark on ill-typed terms ... *)
+
+let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div =
+  check_required_library (cdir@["Ring_base"]);
+  let env = Global.env() in
+  let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
+  let evd = ref sigma in
+  let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
+  let (pow_tac, pspec) = interp_power env evd power in
+  let sspec = interp_sign env evd sign in
+  let dspec = interp_div env evd div in
+  let rk = reflect_coeff morphth in
+  let params,ctx =
+    exec_tactic env !evd 5 (zltac "ring_lemmas")
+      [sth;ext;rth;pspec;sspec;dspec;rk] in
+  let lemma1 = params.(3) in
+  let lemma2 = params.(4) in
+
+  let lemma1 =
+    decl_constant name "_ring_lemma1" ctx lemma1 in
+  let lemma2 =
+    decl_constant name "_ring_lemma2" ctx lemma2 in
+  let cst_tac =
+    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
+  let pretac =
+    match pre with
+        Some t -> Tacintern.glob_tactic t
+      | _ -> TacId [] in
+  let posttac =
+    match post with
+        Some t -> Tacintern.glob_tactic t
+      | _ -> TacId [] in
+  let r = EConstr.to_constr sigma r in
+  let req = EConstr.to_constr sigma req in
+  let sth = EConstr.to_constr sigma sth in
+  let _ =
+    Lib.add_anonymous_leaf
+      (theory_to_obj
+        { ring_name = name;
+          ring_carrier = r;
+          ring_req = req;
+          ring_setoid = sth;
+          ring_ext = params.(1);
+          ring_morph = params.(2);
+          ring_th = params.(0);
+          ring_cst_tac = cst_tac;
+          ring_pow_tac = pow_tac;
+          ring_lemma1 = lemma1;
+          ring_lemma2 = lemma2;
+          ring_pre_tac = pretac;
+          ring_post_tac = posttac }) in
+  ()
+
+let ic_coeff_spec = function
+  | Computational t -> Computational (ic_unsafe t)
+  | Morphism t -> Morphism (ic_unsafe t)
+  | Abstract -> Abstract
+
+
+let set_once s r v =
+  if Option.is_empty !r then r := Some v else error (s^" cannot be set twice")
+
+let process_ring_mods l =
+  let kind = ref None in
+  let set = ref None in
+  let cst_tac = ref None in
+  let pre = ref None in
+  let post = ref None in
+  let sign = ref None in
+  let power = ref None in
+  let div = ref None in
+  List.iter(function
+      Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k)
+    | Const_tac t -> set_once "tactic recognizing constants" cst_tac t
+    | Pre_tac t -> set_once "preprocess tactic" pre t
+    | Post_tac t -> set_once "postprocess tactic" post t
+    | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
+    | Pow_spec(t,spec) -> set_once "power" power (t,spec)
+    | Sign_spec t -> set_once "sign" sign t
+    | Div_spec t -> set_once "div" div t) l;
+  let k = match !kind with Some k -> k | None -> Abstract in
+  (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
+
+let add_theory id rth l =
+  let (sigma, rth) = ic rth in
+  let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
+  add_theory0 id (sigma, rth) set k cst (pre,post) power sign div
+
+(*****************************************************************************)
+(* The tactics consist then only in a lookup in the ring database and
+   call the appropriate ltac. *)
+
+let make_args_list sigma rl t =
+  match rl with
+  | [] -> let (_,t1,t2) = dest_rel0 sigma t in [t1;t2]
+  | _ -> rl
+
+let make_term_list env evd carrier rl =
+  let l = List.fold_right
+    (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
+    (plapp evd coq_nil [|carrier|])
+  in
+  let sigma, l = Typing.solve_evars env !evd l in
+  evd := sigma; l
+
+let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
+let tacarg expr =
+  Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr
+
+let ltac_ring_structure e =
+  let req = carg e.ring_req in
+  let sth = carg e.ring_setoid in
+  let ext = carg e.ring_ext in
+  let morph = carg e.ring_morph in
+  let th = carg e.ring_th in
+  let cst_tac = tacarg e.ring_cst_tac in
+  let pow_tac = tacarg e.ring_pow_tac in
+  let lemma1 = carg e.ring_lemma1 in
+  let lemma2 = carg e.ring_lemma2 in
+  let pretac = tacarg (TacFun([Anonymous],e.ring_pre_tac)) in
+  let posttac = tacarg (TacFun([Anonymous],e.ring_post_tac)) in
+  [req;sth;ext;morph;th;cst_tac;pow_tac;
+   lemma1;lemma2;pretac;posttac]
+
+let ring_lookup (f : Value.t) lH rl t =
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Tacmach.New.project gl in
+    let env = Proofview.Goal.env gl in
+    let rl = make_args_list sigma rl t in
+    let evdref = ref sigma in
+    let e = find_ring_structure env sigma rl in
+    let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
+    let lH = carg (make_hyp_list env evdref lH) in
+    let ring = ltac_ring_structure e in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
+  end
+
+(***********************************************************************)
+
+let new_field_path =
+  DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
+
+let field_ltac s =
+  lazy(KerName.make (ModPath.MPfile new_field_path) (Label.make s))
+
+
+let _ = add_map "field"
+  (map_with_eq
+    [coq_cons,(function -1->Eval|2->Rec|_->Prot);
+    coq_nil, (function -1->Eval|_ -> Prot);
+    my_reference "IDphi", (function _->Eval);
+    my_reference "gen_phiZ", (function _->Eval);
+    (* display_linear: evaluate polynomials and coef operations, protect
+       field operations and make recursive call on the var map *)
+    my_reference "display_linear",
+      (function -1|9|10|11|13|15|16->Eval|12|14->Rec|_->Prot);
+    my_reference "display_pow_linear",
+     (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot);
+   (* Pphi_dev: evaluate polynomial and coef operations, protect
+       ring operations and make recursive call on the var map *)
+    pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
+    pol_cst "Pphi_pow",
+          (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
+    (* PEeval: evaluate polynomial, protect ring
+       operations and make recursive call on the var map *)
+    pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot);
+    (* FEeval: evaluate polynomial, protect field
+       operations and make recursive call on the var map *)
+    my_reference "FEeval", (function -1|12|15->Eval|10|14->Rec|_->Prot)]);;
+
+let _ = add_map "field_cond"
+  (map_without_eq
+    [coq_cons,(function -1->Eval|2->Rec|_->Prot);
+     coq_nil, (function -1->Eval|_ -> Prot);
+     my_reference "IDphi", (function _->Eval);
+     my_reference "gen_phiZ", (function _->Eval);
+    (* PCond: evaluate denum list, protect ring
+       operations and make recursive call on the var map *)
+     my_reference "PCond", (function -1|11|14->Eval|9|13->Rec|_->Prot)]);;
+
+
+let _ = Redexpr.declare_reduction "simpl_field_expr"
+  (protect_red "field")
+
+
+
+let afield_theory = my_reference "almost_field_theory"
+let field_theory = my_reference "field_theory"
+let sfield_theory = my_reference "semi_field_theory"
+let af_ar = my_reference"AF_AR"
+let f_r = my_reference"F_R"
+let sf_sr = my_reference"SF_SR"
+let dest_field env evd th_spec =
+  let th_typ = Retyping.get_type_of env !evd th_spec in
+  match EConstr.kind !evd th_typ with
+    | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
+        when isRefX !evd (Lazy.force afield_theory) f ->
+        let rth = plapp evd af_ar
+          [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
+        (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
+    | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
+        when isRefX !evd (Lazy.force field_theory) f ->
+        let rth =
+          plapp evd f_r
+            [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
+        (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
+    | App(f,[|r;zero;one;add;mul;div;inv;req|])
+        when isRefX !evd (Lazy.force sfield_theory) f ->
+        let rth = plapp evd sf_sr
+          [|r;zero;one;add;mul;div;inv;req;th_spec|] in
+        (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
+    | _ -> error "bad field structure"
+
+let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
+
+let print_fields () =
+  Feedback.msg_notice (strbrk "The following field structures have been declared:");
+  Cmap.iter (fun _carrier fi ->
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
+      Feedback.msg_notice
+        (hov 2
+           (Id.print fi.field_name ++ spc() ++
+            str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
+            str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
+    ) !field_from_carrier
+
+let field_for_carrier r = Cmap.find r !field_from_carrier
+
+let find_field_structure env sigma l =
+  check_required_library (cdir@["Field_tac"]);
+  match l with
+    | t::cl' ->
+        let ty = Retyping.get_type_of env sigma t in
+        let check c =
+          let ty' = Retyping.get_type_of env sigma c in
+          if not (Reductionops.is_conv env sigma ty ty') then
+            CErrors.user_err ~hdr:"field"
+              (str"arguments of field_simplify do not have all the same type")
+        in
+        List.iter check cl';
+        (try field_for_carrier (EConstr.to_constr sigma ty)
+        with Not_found ->
+          CErrors.user_err ~hdr:"field"
+            (str"cannot find a declared field structure over"++
+             spc()++str"\""++pr_econstr_env env sigma ty++str"\""))
+    | [] -> assert false
+
+let add_field_entry e =
+  field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier
+
+let subst_th (subst,th) =
+  let c' = subst_mps subst th.field_carrier in
+  let eq' = subst_mps subst th.field_req in
+  let thm1' = subst_mps subst th.field_ok in
+  let thm2' = subst_mps subst th.field_simpl_eq_ok in
+  let thm3' = subst_mps subst th.field_simpl_ok in
+  let thm4' = subst_mps subst th.field_simpl_eq_in_ok in
+  let thm5' = subst_mps subst th.field_cond in
+  let tac'= Tacsubst.subst_tactic subst th.field_cst_tac in
+  let pow_tac' = Tacsubst.subst_tactic subst th.field_pow_tac in
+  let pretac'= Tacsubst.subst_tactic subst th.field_pre_tac in
+  let posttac'= Tacsubst.subst_tactic subst th.field_post_tac in
+  if c' == th.field_carrier &&
+     eq' == th.field_req &&
+     thm1' == th.field_ok &&
+     thm2' == th.field_simpl_eq_ok &&
+     thm3' == th.field_simpl_ok &&
+     thm4' == th.field_simpl_eq_in_ok &&
+     thm5' == th.field_cond &&
+     tac' == th.field_cst_tac &&
+     pow_tac' == th.field_pow_tac &&
+     pretac' == th.field_pre_tac &&
+     posttac' == th.field_post_tac then th
+  else
+    { field_name = th.field_name;
+      field_carrier = c';
+      field_req = eq';
+      field_cst_tac = tac';
+      field_pow_tac = pow_tac';
+      field_ok = thm1';
+      field_simpl_eq_ok = thm2';
+      field_simpl_ok = thm3';
+      field_simpl_eq_in_ok = thm4';
+      field_cond = thm5';
+      field_pre_tac = pretac';
+      field_post_tac = posttac' }
+
+let ftheory_to_obj : field_info -> obj =
+  let cache_th (_, th) = add_field_entry th in
+  declare_object @@ global_object_nodischarge "tactic-new-field-theory"
+    ~cache:cache_th
+    ~subst:(Some subst_th)
+
+let field_equality evd r inv req =
+  match EConstr.kind !evd req with
+    | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
+        let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in
+        let c = EConstr.of_constr c in
+        mkApp(c,[|r;r;inv|])
+    | _ ->
+        let _setoid = setoid_of_relation (Global.env ()) evd r req in
+        let signature = [Some (r,Some req)],Some(r,Some req) in
+        let inv_m, inv_m_lem =
+          try Rewrite.default_morphism signature inv
+          with Not_found ->
+            error "field inverse should be declared as a morphism" in
+          inv_m_lem
+
+let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
+  let open Constr in
+  check_required_library (cdir@["Field_tac"]);
+  let (sigma,fth) = ic fth in
+  let env = Global.env() in
+  let evd = ref sigma in
+  let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
+    dest_field env evd fth in
+  let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
+  let eqth = Some(sth,ext) in
+  let _ = add_theory0 name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in
+  let (pow_tac, pspec) = interp_power env evd power in
+  let sspec = interp_sign env evd sign in
+  let dspec = interp_div env evd odiv in
+  let inv_m = field_equality evd r inv req in
+  let rk = reflect_coeff morphth in
+  let params,ctx =
+    exec_tactic env !evd 9 (field_ltac"field_lemmas")
+      [sth;ext;inv_m;fth;pspec;sspec;dspec;rk] in
+  let lemma1 = params.(3) in
+  let lemma2 = params.(4) in
+  let lemma3 = params.(5) in
+  let lemma4 = params.(6) in
+  let cond_lemma =
+    match inj with
+      | Some thm -> mkApp(params.(8),[|EConstr.to_constr sigma thm|])
+      | None -> params.(7) in
+  let lemma1 = decl_constant name "_field_lemma1"
+    ctx lemma1 in
+  let lemma2 = decl_constant name "_field_lemma2"
+    ctx lemma2 in
+  let lemma3 = decl_constant name "_field_lemma3"
+    ctx lemma3 in
+  let lemma4 = decl_constant name "_field_lemma4"
+    ctx lemma4 in
+  let cond_lemma = decl_constant name "_lemma5"
+    ctx cond_lemma in
+  let cst_tac =
+    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
+  let pretac =
+    match pre with
+        Some t -> Tacintern.glob_tactic t
+      | _ -> TacId [] in
+  let posttac =
+    match post with
+        Some t -> Tacintern.glob_tactic t
+      | _ -> TacId [] in
+  let r = EConstr.to_constr sigma r in
+  let req = EConstr.to_constr sigma req in
+  let _ =
+    Lib.add_anonymous_leaf
+      (ftheory_to_obj
+        { field_name = name;
+          field_carrier = r;
+          field_req = req;
+          field_cst_tac = cst_tac;
+          field_pow_tac = pow_tac;
+          field_ok = lemma1;
+          field_simpl_eq_ok = lemma2;
+          field_simpl_ok = lemma3;
+          field_simpl_eq_in_ok = lemma4;
+          field_cond = cond_lemma;
+          field_pre_tac = pretac;
+          field_post_tac = posttac }) in  ()
+
+let process_field_mods l =
+  let kind = ref None in
+  let set = ref None in
+  let cst_tac = ref None in
+  let pre = ref None in
+  let post = ref None in
+  let inj = ref None in
+  let sign = ref None in
+  let power = ref None in
+  let div = ref None in
+  List.iter(function
+      Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k)
+    | Ring_mod(Const_tac t) ->
+        set_once "tactic recognizing constants" cst_tac t
+    | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
+    | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t
+    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
+    | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec)
+    | Ring_mod(Sign_spec t) -> set_once "sign" sign t
+    | Ring_mod(Div_spec t) -> set_once "div" div t
+    | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l;
+  let k = match !kind with Some k -> k | None -> Abstract in
+  (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
+
+let add_field_theory id t mods =
+  let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods mods in
+  add_field_theory0 id t set k cst_tac inj (pre,post) power sign div
+
+let ltac_field_structure e =
+  let req = carg e.field_req in
+  let cst_tac = tacarg e.field_cst_tac in
+  let pow_tac = tacarg e.field_pow_tac in
+  let field_ok = carg e.field_ok in
+  let field_simpl_ok = carg e.field_simpl_ok in
+  let field_simpl_eq_ok = carg e.field_simpl_eq_ok in
+  let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in
+  let cond_ok = carg e.field_cond in
+  let pretac = tacarg (TacFun([Anonymous],e.field_pre_tac)) in
+  let posttac = tacarg (TacFun([Anonymous],e.field_post_tac)) in
+  [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
+   field_simpl_eq_in_ok;cond_ok;pretac;posttac]
+
+let field_lookup (f : Value.t) lH rl t =
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Tacmach.New.project gl in
+    let env = Proofview.Goal.env gl in
+    let rl = make_args_list sigma rl t in
+    let evdref = ref sigma in
+    let e = find_field_structure env sigma rl in
+    let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
+    let lH = carg (make_hyp_list env evdref lH) in
+    let field = ltac_field_structure e in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
+  end
diff --git a/plugins/ring/ring.mli b/plugins/ring/ring.mli
new file mode 100644
index 0000000000..6d24ae84d7
--- /dev/null
+++ b/plugins/ring/ring.mli
@@ -0,0 +1,42 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open EConstr
+open Constrexpr
+open Ring_ast
+
+val protect_tac_in : string -> Id.t -> unit Proofview.tactic
+
+val protect_tac : string -> unit Proofview.tactic
+
+val add_theory :
+  Id.t ->
+  constr_expr ->
+  constr_expr ring_mod list -> unit
+
+val print_rings : unit -> unit
+
+val ring_lookup :
+  Geninterp.Val.t ->
+  constr list ->
+  constr list -> constr -> unit Proofview.tactic
+
+val add_field_theory :
+  Id.t ->
+  constr_expr ->
+  constr_expr field_mod list -> unit
+
+val print_fields : unit -> unit
+
+val field_lookup :
+  Geninterp.Val.t ->
+  constr list ->
+  constr list -> constr -> unit Proofview.tactic
diff --git a/plugins/ring/ring_ast.ml b/plugins/ring/ring_ast.ml
new file mode 100644
index 0000000000..8b82783db9
--- /dev/null
+++ b/plugins/ring/ring_ast.ml
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+open Libnames
+open Constrexpr
+
+open Ltac_plugin
+open Tacexpr
+
+type 'constr coeff_spec =
+    Computational of 'constr (* equality test *)
+  | Abstract (* coeffs = Z *)
+  | Morphism of 'constr (* general morphism *)
+
+type cst_tac_spec =
+    CstTac of raw_tactic_expr
+  | Closed of qualid list
+
+type 'constr ring_mod =
+    Ring_kind of 'constr coeff_spec
+  | Const_tac of cst_tac_spec
+  | Pre_tac of raw_tactic_expr
+  | Post_tac of raw_tactic_expr
+  | Setoid of constr_expr * constr_expr
+  | Pow_spec of cst_tac_spec * constr_expr
+           (* Syntaxification tactic , correctness lemma *)
+  | Sign_spec of constr_expr
+  | Div_spec of constr_expr
+
+type 'constr field_mod =
+    Ring_mod of 'constr ring_mod
+  | Inject of constr_expr
+
+type ring_info =
+    { ring_name : Names.Id.t;
+      ring_carrier : types;
+      ring_req : constr;
+      ring_setoid : constr;
+      ring_ext : constr;
+      ring_morph : constr;
+      ring_th : constr;
+      ring_cst_tac : glob_tactic_expr;
+      ring_pow_tac : glob_tactic_expr;
+      ring_lemma1 : constr;
+      ring_lemma2 : constr;
+      ring_pre_tac : glob_tactic_expr;
+      ring_post_tac : glob_tactic_expr }
+
+type field_info =
+    { field_name : Names.Id.t;
+      field_carrier : types;
+      field_req : constr;
+      field_cst_tac : glob_tactic_expr;
+      field_pow_tac : glob_tactic_expr;
+      field_ok : constr;
+      field_simpl_eq_ok : constr;
+      field_simpl_ok : constr;
+      field_simpl_eq_in_ok : constr;
+      field_cond : constr;
+      field_pre_tac : glob_tactic_expr;
+      field_post_tac : glob_tactic_expr }
diff --git a/plugins/ring/ring_ast.mli b/plugins/ring/ring_ast.mli
new file mode 100644
index 0000000000..8b82783db9
--- /dev/null
+++ b/plugins/ring/ring_ast.mli
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+open Libnames
+open Constrexpr
+
+open Ltac_plugin
+open Tacexpr
+
+type 'constr coeff_spec =
+    Computational of 'constr (* equality test *)
+  | Abstract (* coeffs = Z *)
+  | Morphism of 'constr (* general morphism *)
+
+type cst_tac_spec =
+    CstTac of raw_tactic_expr
+  | Closed of qualid list
+
+type 'constr ring_mod =
+    Ring_kind of 'constr coeff_spec
+  | Const_tac of cst_tac_spec
+  | Pre_tac of raw_tactic_expr
+  | Post_tac of raw_tactic_expr
+  | Setoid of constr_expr * constr_expr
+  | Pow_spec of cst_tac_spec * constr_expr
+           (* Syntaxification tactic , correctness lemma *)
+  | Sign_spec of constr_expr
+  | Div_spec of constr_expr
+
+type 'constr field_mod =
+    Ring_mod of 'constr ring_mod
+  | Inject of constr_expr
+
+type ring_info =
+    { ring_name : Names.Id.t;
+      ring_carrier : types;
+      ring_req : constr;
+      ring_setoid : constr;
+      ring_ext : constr;
+      ring_morph : constr;
+      ring_th : constr;
+      ring_cst_tac : glob_tactic_expr;
+      ring_pow_tac : glob_tactic_expr;
+      ring_lemma1 : constr;
+      ring_lemma2 : constr;
+      ring_pre_tac : glob_tactic_expr;
+      ring_post_tac : glob_tactic_expr }
+
+type field_info =
+    { field_name : Names.Id.t;
+      field_carrier : types;
+      field_req : constr;
+      field_cst_tac : glob_tactic_expr;
+      field_pow_tac : glob_tactic_expr;
+      field_ok : constr;
+      field_simpl_eq_ok : constr;
+      field_simpl_ok : constr;
+      field_simpl_eq_in_ok : constr;
+      field_cond : constr;
+      field_pre_tac : glob_tactic_expr;
+      field_post_tac : glob_tactic_expr }
diff --git a/plugins/ring/ring_plugin.mlpack b/plugins/ring/ring_plugin.mlpack
new file mode 100644
index 0000000000..91d7199f9b
--- /dev/null
+++ b/plugins/ring/ring_plugin.mlpack
@@ -0,0 +1,3 @@
+Ring_ast
+Ring
+G_ring