summaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /plugins/setoid_ring
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/ArithRing.v4
-rw-r--r--plugins/setoid_ring/InitialRing.v50
-rw-r--r--plugins/setoid_ring/NArithRing.v2
-rw-r--r--plugins/setoid_ring/Ncring_initial.v4
-rw-r--r--plugins/setoid_ring/Ring.v6
-rw-r--r--plugins/setoid_ring/Ring_polynom.v2
-rw-r--r--plugins/setoid_ring/Ring_tac.v2
-rw-r--r--plugins/setoid_ring/Ring_theory.v5
-rw-r--r--plugins/setoid_ring/ZArithRing.v8
-rw-r--r--plugins/setoid_ring/g_newring.ml4133
-rw-r--r--plugins/setoid_ring/newring.ml (renamed from plugins/setoid_ring/newring.ml4)319
-rw-r--r--plugins/setoid_ring/newring.mli78
-rw-r--r--plugins/setoid_ring/newring_ast.mli63
-rw-r--r--plugins/setoid_ring/newring_plugin.mllib2
-rw-r--r--plugins/setoid_ring/newring_plugin.mlpack2
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