Imported Upstream version 8.6upstream/8.6

15 files changed, 403 insertions, 277 deletions

diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 04decbce..5f5b9792 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -32,13 +32,13 @@ Qed.
 Ltac natcst t :=
   match isnatcst t with
     true => constr:(N.of_nat t)
-  | _ => constr:InitialRing.NotConstant
+  | _ => constr:(InitialRing.NotConstant)
   end.
 
 Ltac Ss_to_add f acc :=
   match f with
   | S ?f1 => Ss_to_add f1 (S acc)
-  | _ => constr:(acc + f)%nat
+  | _ => constr:((acc + f)%nat)
   end.
 
 Ltac natprering :=
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 8362c8c2..9c690e2b 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -96,7 +96,7 @@ Section ZMORPHISM.
  Proof.
   constructor.
   destruct c;intros;try discriminate.
-  injection H;clear H;intros H1;subst c'.
+  injection H as <-.
   simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
  Qed.
 
@@ -612,32 +612,32 @@ End GEN_DIV.
  Ltac inv_gen_phi_pos rI add mul t :=
    let rec inv_cst t :=
    match t with
-     rI => constr:1%positive
-   | (add rI rI) => constr:2%positive
-   | (add rI (add rI rI)) => constr:3%positive
+     rI => constr:(1%positive)
+   | (add rI rI) => constr:(2%positive)
+   | (add rI (add rI rI)) => constr:(3%positive)
    | (mul (add rI rI) ?p) => (* 2p *)
        match inv_cst p with
-         NotConstant => constr:NotConstant
-       | 1%positive => constr:NotConstant (* 2*1 is not convertible to 2 *)
+         NotConstant => constr:(NotConstant)
+       | 1%positive => constr:(NotConstant) (* 2*1 is not convertible to 2 *)
        | ?p => constr:(xO p)
        end
    | (add rI (mul (add rI rI) ?p)) => (* 1+2p *)
        match inv_cst p with
-         NotConstant => constr:NotConstant
-       | 1%positive => constr:NotConstant
+         NotConstant => constr:(NotConstant)
+       | 1%positive => constr:(NotConstant)
        | ?p => constr:(xI p)
        end
-   | _ => constr:NotConstant
+   | _ => constr:(NotConstant)
    end in
    inv_cst t.
 
 (* The (partial) inverse of gen_phiNword *)
  Ltac inv_gen_phiNword rO rI add mul opp t :=
    match t with
-     rO => constr:NwO
+     rO => constr:(NwO)
    | _ =>
      match inv_gen_phi_pos rI add mul t with
-       NotConstant => constr:NotConstant
+       NotConstant => constr:(NotConstant)
      | ?p => constr:(Npos p::nil)
      end
    end.
@@ -646,10 +646,10 @@ End GEN_DIV.
 (* The inverse of gen_phiN *)
  Ltac inv_gen_phiN rO rI add mul t :=
    match t with
-     rO => constr:0%N
+     rO => constr:(0%N)
    | _ =>
      match inv_gen_phi_pos rI add mul t with
-       NotConstant => constr:NotConstant
+       NotConstant => constr:(NotConstant)
      | ?p => constr:(Npos p)
      end
    end.
@@ -657,15 +657,15 @@ End GEN_DIV.
 (* The inverse of gen_phiZ *)
  Ltac inv_gen_phiZ rO rI add mul opp t :=
    match t with
-     rO => constr:0%Z
+     rO => constr:(0%Z)
    | (opp ?p) =>
      match inv_gen_phi_pos rI add mul p with
-       NotConstant => constr:NotConstant
+       NotConstant => constr:(NotConstant)
      | ?p => constr:(Zneg p)
      end
    | _ =>
      match inv_gen_phi_pos rI add mul t with
-       NotConstant => constr:NotConstant
+       NotConstant => constr:(NotConstant)
      | ?p => constr:(Zpos p)
      end
    end.
@@ -681,7 +681,7 @@ Ltac inv_gen_phi rO rI cO cI t :=
   end.
 
 (* A simple tactic recognizing no constant *)
- Ltac inv_morph_nothing t := constr:NotConstant.
+ Ltac inv_morph_nothing t := constr:(NotConstant).
 
 Ltac coerce_to_almost_ring set ext rspec :=
   match type of rspec with
@@ -825,31 +825,31 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk :=
 (* Tactic for constant *)
 Ltac isnatcst t :=
   match t with
-    O => constr:true
+    O => constr:(true)
   | S ?p => isnatcst p
-  | _ => constr:false
+  | _ => constr:(false)
   end.
 
 Ltac isPcst t :=
   match t with
   | xI ?p => isPcst p
   | xO ?p => isPcst p
-  | xH => constr:true
+  | xH => constr:(true)
   (* nat -> positive *)
   | Pos.of_succ_nat ?n => isnatcst n
-  | _ => constr:false
+  | _ => constr:(false)
   end.
 
 Ltac isNcst t :=
   match t with
-    N0 => constr:true
+    N0 => constr:(true)
   | Npos ?p => isPcst p
-  | _ => constr:false
+  | _ => constr:(false)
   end.
 
 Ltac isZcst t :=
   match t with
-    Z0 => constr:true
+    Z0 => constr:(true)
   | Zpos ?p => isPcst p
   | Zneg ?p => isPcst p
   (* injection nat -> Z *)
@@ -857,7 +857,7 @@ Ltac isZcst t :=
   (* injection N -> Z *)
   | Z.of_N ?n => isNcst n
   (* *)
-  | _ => constr:false
+  | _ => constr:(false)
   end.
 
 
diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v
index 6c1a79e4..54e2789b 100644
--- a/plugins/setoid_ring/NArithRing.v
+++ b/plugins/setoid_ring/NArithRing.v
@@ -15,7 +15,7 @@ Set Implicit Arguments.
 Ltac Ncst t :=
   match isNcst t with
     true => t
-  | _ => constr:NotConstant
+  | _ => constr:(NotConstant)
   end.
 
 Add Ring Nr : Nth (decidable Neqb_ok, constants [Ncst]).
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 96885d2f..20022c00 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -18,7 +18,6 @@ Require Import BinInt.
 Require Import Setoid.
 Require Export Ncring.
 Require Export Ncring_polynom.
-Import List.
 
 Set Implicit Arguments.
 
@@ -78,7 +77,8 @@ Context {R:Type}`{Ring R}.
   | Z0 => 0
   | Zneg p => -(gen_phiPOS p)
   end.
- Notation "[ x ]" := (gen_phiZ x).
+ Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
+ Local Open Scope ZMORPHISM.
 
  Definition get_signZ z :=
   match z with
diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v
index a0844100..77576cb9 100644
--- a/plugins/setoid_ring/Ring.v
+++ b/plugins/setoid_ring/Ring.v
@@ -36,9 +36,9 @@ Qed.
 Ltac bool_cst t :=
   let t := eval hnf in t in
   match t with
-    true => constr:true
-  | false => constr:false
-  | _ => constr:NotConstant
+    true => constr:(true)
+  | false => constr:(false)
+  | _ => constr:(NotConstant)
   end.
 
 Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]).
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 760ad4da..b6919667 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -883,7 +883,7 @@ Section MakeRingPol.
  revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros.
  - discriminate.
  - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst.
-   * injection H; intros <-. rewrite <- PSubstL1_ok; intuition.
+   * injection H as <-. rewrite <- PSubstL1_ok; intuition.
    * now apply IH.
  Qed.
 
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 77863edc..fc02cef1 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -422,8 +422,6 @@ Tactic Notation (at level 0)
   let G := Get_goal in
   ring_lookup (PackRing Ring_simplify) [lH] rl G.
 
-(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *)
-
 Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
   let G := Get_goal in
   let t := type of H in
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 7fcd6c08..f7757a18 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -238,7 +238,6 @@ Section ALMOST_RING.
  Variable req : R -> R -> Prop.
  Notation "0" := rO.  Notation "1" := rI.
  Infix "==" := req. Infix "+" := radd.  Infix "* " := rmul.
- Infix "-" := rsub. Notation "- x" := (ropp x).
 
  (** Leibniz equality leads to a setoid theory and is extensional*)
  Lemma Eqsth : Equivalence (@eq R).
@@ -263,7 +262,7 @@ Section ALMOST_RING.
         -x = x and x - y = x + y *)
  Definition SRopp (x:R) := x. Notation "- x" := (SRopp x).
 
- Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y).
+ Definition SRsub x y := x + -y. Infix "-" := SRsub.
 
  Lemma SRopp_ext : forall x y, x == y -> -x == -y.
  Proof. intros x y H; exact H. Qed.
@@ -320,6 +319,8 @@ Section ALMOST_RING.
  Qed.
 
  End  SEMI_RING.
+ Infix "-" := rsub.
+ Notation "- x" := (ropp x).
 
  Variable Reqe : ring_eq_ext radd rmul ropp req.
    Add Morphism radd : radd_ext2.  exact (Radd_ext Reqe). Qed.
diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 91484372..23784cf3 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -17,14 +17,14 @@ Set Implicit Arguments.
 Ltac Zcst t :=
   match isZcst t with
     true => t
-  | _ => constr:NotConstant
+  | _ => constr:(NotConstant)
   end.
 
 Ltac isZpow_coef t :=
   match t with
   | Zpos ?p => isPcst p
-  | Z0 => constr:true
-  | _ => constr:false
+  | Z0 => constr:(true)
+  | _ => constr:(false)
   end.
 
 Notation N_of_Z := Z.to_N (only parsing).
@@ -32,7 +32,7 @@ Notation N_of_Z := Z.to_N (only parsing).
 Ltac Zpow_tac t :=
  match isZpow_coef t with
  | true => constr:(N_of_Z t)
- | _ => constr:NotConstant
+ | _ => constr:(NotConstant)
  end.
 
 Ltac Zpower_neg :=
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
new file mode 100644
index 00000000..216eb8b3
--- /dev/null
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -0,0 +1,133 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+open Pp
+open Util
+open Libnames
+open Printer
+open Newring_ast
+open Newring
+open Stdarg
+open Constrarg
+open Pcoq.Constr
+open Pcoq.Tactic
+
+DECLARE PLUGIN "newring_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
+
+TACTIC EXTEND closed_term
+  [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
+    [ closed_term t l ]
+END
+
+open Pptactic
+open Ppconstr
+
+let pr_ring_mod = function
+  | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg pr_constr_expr eq_test
+  | Ring_kind Abstract ->  str "abstract"
+  | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph
+  | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
+  | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]"
+  | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
+  | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
+  | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext
+  | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]"
+  | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
+  | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t
+  | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t
+
+VERNAC ARGUMENT EXTEND ring_mod
+  PRINTED BY pr_ring_mod
+  | [ "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 l = surround (prlist_with_sep pr_comma pr_ring_mod l)
+
+VERNAC ARGUMENT EXTEND ring_mods
+  PRINTED BY pr_ring_mods
+  | [ "(" 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) ] ->
+    [ let l = match l with None -> [] | Some l -> l in
+      let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
+      add_theory id (ic t) set k cst (pre,post) power sign div]
+  | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
+    Feedback.msg_notice (strbrk "The following ring structures have been declared:");
+    Spmap.iter (fun fn fi ->
+      Feedback.msg_notice (hov 2
+        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+          str"with carrier "++ pr_constr fi.ring_carrier++spc()++
+          str"and equivalence relation "++ pr_constr fi.ring_req))
+    ) !from_name ]
+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 = function
+  | Ring_mod m -> pr_ring_mod m
+  | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj
+
+VERNAC ARGUMENT EXTEND field_mod
+  PRINTED BY pr_field_mod
+  | [ ring_mod(m) ] -> [ Ring_mod m ]
+  | [ "completeness" constr(inj) ] -> [ Inject inj ]
+END
+
+let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l)
+
+VERNAC ARGUMENT EXTEND field_mods
+  PRINTED BY pr_field_mods
+  | [ "(" 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
+    let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
+    add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
+| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
+    Feedback.msg_notice (strbrk "The following field structures have been declared:");
+    Spmap.iter (fun fn fi ->
+      Feedback.msg_notice (hov 2
+        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+          str"with carrier "++ pr_constr fi.field_carrier++spc()++
+          str"and equivalence relation "++ pr_constr fi.field_req))
+    ) !field_from_name ]
+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/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml
index e704c466..90f5f8e6 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml
@@ -6,15 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
 open Vars
-open Closure
+open CClosure
 open Environ
 open Libnames
 open Globnames
@@ -30,21 +28,12 @@ open Declare
 open Decl_kinds
 open Entries
 open Misctypes
-
-DECLARE PLUGIN "newring_plugin"
+open Newring_ast
+open Proofview.Notations
 
 (****************************************************************************)
 (* controlled reduction *)
 
-(** ppedrot: something dubious here, we're obviously using evars the wrong
-    way. FIXME! *)
-
-let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|])
-let unmark_arg f c =
-  match destEvar c with
-    | (i,[|c|]) -> f (Evar.repr i) c
-    | _ -> assert false
-
 type protect_flag = Eval|Prot|Rec
 
 let tag_arg tag_rec map subs i c =
@@ -77,12 +66,10 @@ and mk_clos_app_but f_map subs f args n =
     let fargs, args' = Array.chop n args in
     let f' = mkApp(f,fargs) in
     match f_map (global_of_constr_nofail f') with
-        Some map ->
-          mk_clos_deep
-            (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s'))
-            subs
-            (mkApp (mark_arg (-1) f', Array.mapi mark_arg args'))
-      | None -> mk_clos_app_but f_map subs f args (n+1)
+    | Some map ->
+       let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in
+       mk_red (FApp (f (-1) f', Array.mapi f args'))
+    | None -> mk_atom (mkApp (f, args))
 
 let interp_map l t =
   try Some(List.assoc_f eq_gr t l) with Not_found -> None
@@ -95,36 +82,23 @@ let lookup_map map =
     errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
 
 let protect_red map env sigma c =
-  kl (create_clos_infos betadeltaiota env)
+  kl (create_clos_infos all env)
     (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
 
 let protect_tac map =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
+  Tactics.reduct_option (protect_red map,DEFAULTcast) None
 
 let protect_tac_in map id =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));;
-
+  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))
 
-TACTIC EXTEND protect_fv
-  [ "protect_fv" string(map) "in" ident(id) ] ->
-    [ Proofview.V82.tactic (protect_tac_in map id) ]
-| [ "protect_fv" string(map) ] ->
-    [ Proofview.V82.tactic (protect_tac map) ]
-END;;
 
 (****************************************************************************)
 
 let closed_term t l =
+  let open Quote_plugin in
   let l = List.map Universes.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
-  if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt())
-;;
-
-TACTIC EXTEND closed_term
-  [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
-    [ Proofview.V82.tactic (closed_term t l) ]
-END
-;;
+  if Quote.closed_under cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
 
 (* TACTIC EXTEND echo
 | [ "echo" constr(t) ] ->
@@ -143,11 +117,15 @@ let closed_term_ast l =
     mltac_plugin = "newring_plugin";
     mltac_tactic = "closed_term";
   } in
+  let tacname = {
+    mltac_name = tacname;
+    mltac_index = 0;
+  } in
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
   TacML(Loc.ghost,tacname,
-  [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
-   Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l]))
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
+   TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)]))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)
@@ -164,11 +142,6 @@ let ic_unsafe c = (*FIXME remove *)
   let sigma = Evd.from_env env in
     fst (Constrintern.interp_constr env sigma c)
 
-let ty c =
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
-    Typing.unsafe_type_of env sigma c
-
 let decl_constant na ctx c =
   let vars = Universes.universes_of_constr c in
   let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
@@ -185,18 +158,16 @@ let ltac_call tac (args:glob_tactic_arg list) =
 let ltac_lcall tac args =
   TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args))
 
-let ltac_letin (x, e1) e2 =
-  TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2)
-
-let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) =
-  Tacinterp.eval_tactic
-    (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args))
-
-let ltac_record flds =
-  TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds)
-
-
-let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
+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.ghost, 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
+  let lfun = Id.Map.add (Id.of_string "F") f lfun in
+  let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
+  Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
 
 let dummy_goal env sigma =
   let (gl,_,sigma) = 
@@ -207,20 +178,39 @@ let constr_of v = match Value.to_constr v with
   | Some c -> c
   | None -> failwith "Ring.exec_tactic: anomaly"
 
+let tactic_res = ref [||]
+
+let get_res =
+  let open Tacexpr in
+  let name = { mltac_plugin = "newring_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 (Loc.ghost, 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 res = ref [||] in
-  let get_res ist =
-    let l = List.map (fun id ->  Id.Map.find id ist.lfun) lid in
-    res := Array.of_list l;
-    TacId[] in
-  let getter =
-    Tacexp(TacFun(List.map(fun id -> Some id) lid,
-                  Tacintern.glob_tactic(tacticIn get_res))) in
+  let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
+  let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in
+  let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in
+  (** Evaluate the whole result *)
   let gl = dummy_goal env evd in
-  let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in
+  let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
   let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
-    Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd)
+    Array.map (fun x -> nf (constr_of x)) !tactic_res, snd (Evd.universe_context evd)
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
@@ -281,8 +271,6 @@ let my_reference c =
 
 let new_ring_path =
   DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
-let ltac s =
-  lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s))
 let znew_ring_path =
   DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
@@ -309,21 +297,12 @@ let coq_mk_reqe = my_constant "mk_reqe"
 let coq_semi_ring_theory = my_constant "semi_ring_theory"
 let coq_mk_seqe = my_constant "mk_seqe"
 
-let ltac_inv_morph_gen = zltac"inv_gen_phi"
-let ltac_inv_morphZ = zltac"inv_gen_phiZ"
-let ltac_inv_morphN = zltac"inv_gen_phiN"
-let ltac_inv_morphNword = zltac"inv_gen_phiNword"
 let coq_abstract = my_constant"Abstract"
 let coq_comp = my_constant"Computational"
 let coq_morph = my_constant"Morphism"
 
-(* morphism *)
-let coq_ring_morph = my_constant "ring_morph"
-let coq_semi_morph = my_constant "semi_morph"
-
 (* power function *)
 let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
-let coq_pow_N_pow_N = my_constant "pow_N_pow_N"
 
 (* hypothesis *)
 let coq_mkhypo = my_reference "mkhypo"
@@ -355,20 +334,6 @@ let _ = add_map "ring"
 (****************************************************************************)
 (* Ring database *)
 
-type ring_info =
-    { 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 }
-
 module Cmap = Map.Make(Constr)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
@@ -527,8 +492,8 @@ let ring_equality env evd (r,add,mul,opp,req) =
 	  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 setoid = Typing.solve_evars env evd setoid in
-	let op_morph = Typing.solve_evars env evd op_morph in
+	let setoid = Typing.e_solve_evars env evd setoid in
+	let op_morph = Typing.e_solve_evars env evd op_morph in
 	  (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) evd r req in
@@ -551,7 +516,7 @@ let ring_equality env evd (r,add,mul,opp,req) =
 		let op_morph =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
 		  Flags.if_verbose
-		    msg_info
+		    Feedback.msg_info
 		    (str"Using setoid \""++pr_constr req++str"\""++spc()++
 			str"and morphisms \""++pr_constr add_m_lem ++
 			str"\","++spc()++ str"\""++pr_constr mul_m_lem++
@@ -560,7 +525,7 @@ let ring_equality env evd (r,add,mul,opp,req) =
 		  op_morph)
             | None ->
 		(Flags.if_verbose
-		    msg_info
+		    Feedback.msg_info
 		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
 			str"and morphisms \""++pr_constr add_m_lem ++
 			str"\""++spc()++str"and \""++
@@ -588,25 +553,6 @@ let dest_ring env sigma th_spec =
     | _ -> error "bad ring structure"
 
 
-let dest_morph env sigma m_spec =
-  let m_typ = Retyping.get_type_of env sigma m_spec in
-  match kind_of_term m_typ with
-      App(f,[|r;zero;one;add;mul;sub;opp;req;
-              c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
-        when eq_constr_nounivs f (Lazy.force coq_ring_morph) ->
-          (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
-    | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
-        when eq_constr_nounivs f (Lazy.force coq_semi_morph) ->
-        (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
-    | _ -> error "bad morphism structure"
-
-
-type 'constr coeff_spec =
-    Computational of 'constr (* equality test *)
-  | Abstract (* coeffs = Z *)
-  | Morphism of 'constr (* general morphism *)
-
-
 let reflect_coeff rkind =
   (* We build an ill-typed terms on purpose... *)
   match rkind with
@@ -614,10 +560,6 @@ let reflect_coeff rkind =
     | Computational c -> lapp coq_comp [|c|]
     | Morphism m -> lapp coq_morph [|m|]
 
-type cst_tac_spec =
-    CstTac of raw_tactic_expr
-  | Closed of reference list
-
 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
@@ -638,7 +580,7 @@ let make_hyp_list env evd lH =
       (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
       (plapp evd coq_nil [|carrier|])
   in 
-  let l' = Typing.solve_evars env evd l in
+  let l' = Typing.e_solve_evars env evd l in
     Evarutil.nf_evars_universes !evd l'
 
 let interp_power env evd pow =
@@ -686,7 +628,7 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
   let rk = reflect_coeff morphth in
   let params,ctx =
     exec_tactic env !evd 5 (zltac "ring_lemmas")
-      (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in
+      [sth;ext;rth;pspec;sspec;dspec;rk] in
   let lemma1 = params.(3) in
   let lemma2 = params.(4) in
 
@@ -721,41 +663,12 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
           ring_post_tac = posttac }) in
   ()
 
-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 Constrexpr.constr_expr * Constrexpr.constr_expr
-  | Pow_spec of cst_tac_spec * Constrexpr.constr_expr
-           (* Syntaxification tactic , correctness lemma *)
-  | Sign_spec of Constrexpr.constr_expr
-  | Div_spec of Constrexpr.constr_expr
-
-
 let ic_coeff_spec = function
   | Computational t -> Computational (ic_unsafe t)
   | Morphism t -> Morphism (ic_unsafe t)
   | Abstract -> Abstract
 
 
-VERNAC ARGUMENT EXTEND ring_mod
-  | [ "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 set_once s r v =
   if Option.is_empty !r then r := Some v else error (s^" cannot be set twice")
 
@@ -780,20 +693,6 @@ let process_ring_mods l =
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
-  | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
-    [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
-      add_theory id (ic t) set k cst (pre,post) power sign div]
-  | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
-    msg_notice (strbrk "The following ring structures have been declared:");
-    Spmap.iter (fun fn fi ->
-      msg_notice (hov 2
-        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr fi.ring_carrier++spc()++
-          str"and equivalence relation "++ pr_constr fi.ring_req))
-    ) !from_name ]
-END
-
 (*****************************************************************************)
 (* The tactics consist then only in a lookup in the ring database and
    call the appropriate ltac. *)
@@ -807,7 +706,11 @@ 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 Typing.solve_evars env evd l
+  in Typing.e_solve_evars env evd l
+
+let carg = Tacinterp.Value.of_constr
+let tacarg expr =
+  Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr
 
 let ltac_ring_structure e =
   let req = carg e.ring_req in
@@ -815,18 +718,18 @@ let ltac_ring_structure e =
   let ext = carg e.ring_ext in
   let morph = carg e.ring_morph in
   let th = carg e.ring_th in
-  let cst_tac = Tacexp e.ring_cst_tac in
-  let pow_tac = Tacexp e.ring_pow_tac 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 = Tacexp(TacFun([None],e.ring_pre_tac)) in
-  let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in
+  let pretac = tacarg (TacFun([None],e.ring_pre_tac)) in
+  let posttac = tacarg (TacFun([None],e.ring_post_tac)) in
   [req;sth;ext;morph;th;cst_tac;pow_tac;
    lemma1;lemma2;pretac;posttac]
 
-let ring_lookup (f:glob_tactic_expr) lH rl t =
-  Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
+let ring_lookup (f : Value.t) lH rl t =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     try (* find_ring_strucure can raise an exception *)
       let evdref = ref sigma in
@@ -837,14 +740,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t =
       let ring = ltac_ring_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  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
-
-
+  end }
 
 (***********************************************************************)
 
@@ -919,19 +815,6 @@ let dest_field env evd th_spec =
         (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
     | _ -> error "bad field structure"
 
-type field_info =
-    { 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 }
-
 let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
 let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
 
@@ -1034,7 +917,7 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power
   let rk = reflect_coeff morphth in
   let params,ctx =
     exec_tactic env !evd 9 (field_ltac"field_lemmas")
-      (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in
+      [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
@@ -1078,15 +961,6 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power
           field_pre_tac = pretac;
           field_post_tac = posttac }) in  ()
 
-type 'constr field_mod =
-    Ring_mod of 'constr ring_mod
-  | Inject of Constrexpr.constr_expr
-
-VERNAC ARGUMENT EXTEND field_mod
-  | [ ring_mod(m) ] -> [ Ring_mod m ]
-  | [ "completeness" constr(inj) ] -> [ Inject inj ]
-END
-
 let process_field_mods l =
   let kind = ref None in
   let set = ref None in
@@ -1111,38 +985,23 @@ let process_field_mods l =
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
-| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
-  [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
-    add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
-| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
-    msg_notice (strbrk "The following field structures have been declared:");
-    Spmap.iter (fun fn fi ->
-      msg_notice (hov 2
-        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr fi.field_carrier++spc()++
-          str"and equivalence relation "++ pr_constr fi.field_req))
-    ) !field_from_name ]
-END
-
-
 let ltac_field_structure e =
   let req = carg e.field_req in
-  let cst_tac = Tacexp e.field_cst_tac in
-  let pow_tac = Tacexp e.field_pow_tac 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 = Tacexp(TacFun([None],e.field_pre_tac)) in
-  let posttac = Tacexp(TacFun([None],e.field_post_tac)) in
+  let pretac = tacarg (TacFun([None],e.field_pre_tac)) in
+  let posttac = tacarg (TacFun([None],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:glob_tactic_expr) lH rl t =
-  Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
+let field_lookup (f : Value.t) lH rl t =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     try
       let evdref = ref sigma in
@@ -1153,10 +1012,4 @@ let field_lookup (f:glob_tactic_expr) lH rl t =
       let field = ltac_field_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  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
+  end }
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
new file mode 100644
index 00000000..f417c87c
--- /dev/null
+++ b/plugins/setoid_ring/newring.mli
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Constr
+open Libnames
+open Globnames
+open Constrexpr
+open Tacexpr
+open Proof_type
+open Newring_ast
+
+val protect_tac_in : string -> Id.t -> unit Proofview.tactic
+
+val protect_tac : string -> unit Proofview.tactic
+
+val closed_term : constr -> global_reference list -> unit Proofview.tactic
+
+val process_ring_mods :
+  constr_expr ring_mod list ->
+  constr coeff_spec * (constr * constr) option *
+  cst_tac_spec option * raw_tactic_expr option *
+  raw_tactic_expr option *
+  (cst_tac_spec * constr_expr) option *
+  constr_expr option * constr_expr option
+
+val add_theory :
+  Id.t ->
+  Evd.evar_map * constr ->
+  (constr * constr) option ->
+  constr coeff_spec ->
+  cst_tac_spec option ->
+  raw_tactic_expr option * raw_tactic_expr option ->
+  (cst_tac_spec * constr_expr) option ->
+  constr_expr option ->
+  constr_expr option -> unit
+
+val ic : constr_expr -> Evd.evar_map * constr
+
+val from_name : ring_info Spmap.t ref
+
+val ring_lookup :
+  Geninterp.Val.t ->
+  constr list ->
+  constr list -> constr -> unit Proofview.tactic
+
+val process_field_mods :
+  constr_expr field_mod list ->
+  constr coeff_spec *
+  (constr * constr) option * constr option *
+  cst_tac_spec option * raw_tactic_expr option *
+  raw_tactic_expr option *
+  (cst_tac_spec * constr_expr) option *
+  constr_expr option * constr_expr option
+
+val add_field_theory :
+  Id.t ->
+  Evd.evar_map * constr ->
+  (constr * constr) option ->
+  constr coeff_spec ->
+  cst_tac_spec option ->
+  constr option ->
+  raw_tactic_expr option * raw_tactic_expr option ->
+  (cst_tac_spec * constr_expr) option ->
+  constr_expr option ->
+  constr_expr option -> unit
+
+val field_from_name : field_info Spmap.t ref
+
+val field_lookup :
+  Geninterp.Val.t ->
+  constr list ->
+  constr list -> constr -> unit Proofview.tactic
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
new file mode 100644
index 00000000..c26fcc8d
--- /dev/null
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Constr
+open Libnames
+open Constrexpr
+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 reference 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_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_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/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib
deleted file mode 100644
index a98392f1..00000000
--- a/plugins/setoid_ring/newring_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Newring
-Newring_plugin_mod
diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack
new file mode 100644
index 00000000..23663b40
--- /dev/null
+++ b/plugins/setoid_ring/newring_plugin.mlpack
@@ -0,0 +1,2 @@
+Newring
+G_newring