From 171c7cbc624f399c306c00b9188810bb12f4957e Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 22 Sep 2003 13:22:47 +0000 Subject: tentative de rafraichissement de Setoid Ring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4439 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/ring/g_ring.ml4 | 2 +- contrib/ring/ring.ml | 44 ++++++++++++++++++++++---------------------- 2 files changed, 23 insertions(+), 23 deletions(-) diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4 index a5a02dd76..c4cbd9cf6 100644 --- a/contrib/ring/g_ring.ml4 +++ b/contrib/ring/g_ring.ml4 @@ -94,7 +94,7 @@ VERNAC COMMAND EXTEND AddRing | [ "Add" "Setoid" "Ring" constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult) constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm) - constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ] + constr(mm) constr(om) constr(t) "[" constr_list(l) "]" ] -> [ add_theory true false true (constr_of a) (Some (constr_of aequiv)) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index c360f795a..8adaf75eb 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -71,33 +71,33 @@ let coq_polynomial_simplify_ok = lazy (constant ["ring";"Ring_normalize"] "polynomial_simplify_ok") (* Setoid theory *) -let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory") +let coq_Setoid_Theory = lazy(constant ["Setoids";"Setoid"] "Setoid_Theory") -let coq_seq_refl = lazy(constant ["Setoid"] "Seq_refl") -let coq_seq_sym = lazy(constant ["Setoid"] "Seq_sym") -let coq_seq_trans = lazy(constant ["Setoid"] "Seq_trans") +let coq_seq_refl = lazy(constant ["Setoids";"Setoid"] "Seq_refl") +let coq_seq_sym = lazy(constant ["Setoids";"Setoid"] "Seq_sym") +let coq_seq_trans = lazy(constant ["Setoids";"Setoid"] "Seq_trans") (* Setoid Ring normalize *) -let coq_SetSPplus = lazy (constant ["ring";"Ring_normalize"] "SetSPplus") -let coq_SetSPmult = lazy (constant ["ring";"Ring_normalize"] "SetSPmult") -let coq_SetSPvar = lazy (constant ["ring";"Ring_normalize"] "SetSPvar") -let coq_SetSPconst = lazy (constant ["ring";"Ring_normalize"] "SetSPconst") -let coq_SetPplus = lazy (constant ["ring";"Ring_normalize"] "SetPplus") -let coq_SetPmult = lazy (constant ["ring";"Ring_normalize"] "SetPmult") -let coq_SetPvar = lazy (constant ["ring";"Ring_normalize"] "SetPvar") -let coq_SetPconst = lazy (constant ["ring";"Ring_normalize"] "SetPconst") -let coq_SetPopp = lazy (constant ["ring";"Ring_normalize"] "SetPopp") -let coq_interp_setsp = lazy (constant ["ring";"Ring_normalize"] "interp_setsp") -let coq_interp_setp = lazy (constant ["ring";"Ring_normalize"] "interp_setp") -let coq_interp_setcs = lazy (constant ["ring";"Ring_normalize"] "interp_cs") +let coq_SetSPplus = lazy (constant ["ring";"Setoid_ring_normalize"] "SetSPplus") +let coq_SetSPmult = lazy (constant ["ring";"Setoid_ring_normalize"] "SetSPmult") +let coq_SetSPvar = lazy (constant ["ring";"Setoid_ring_normalize"] "SetSPvar") +let coq_SetSPconst = lazy (constant ["ring";"Setoid_ring_normalize"] "SetSPconst") +let coq_SetPplus = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPplus") +let coq_SetPmult = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPmult") +let coq_SetPvar = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPvar") +let coq_SetPconst = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPconst") +let coq_SetPopp = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPopp") +let coq_interp_setsp = lazy (constant ["ring";"Setoid_ring_normalize"] "interp_setsp") +let coq_interp_setp = lazy (constant ["ring";"Setoid_ring_normalize"] "interp_setp") +let coq_interp_setcs = lazy (constant ["ring";"Setoid_ring_normalize"] "interp_cs") let coq_setspolynomial_simplify = - lazy (constant ["ring";"Ring_normalize"] "setspolynomial_simplify") + lazy (constant ["ring";"Setoid_ring_normalize"] "setspolynomial_simplify") let coq_setpolynomial_simplify = - lazy (constant ["ring";"Ring_normalize"] "setpolynomial_simplify") + lazy (constant ["ring";"Setoid_ring_normalize"] "setpolynomial_simplify") let coq_setspolynomial_simplify_ok = - lazy (constant ["ring";"Ring_normalize"] "setspolynomial_simplify_ok") + lazy (constant ["ring";"Setoid_ring_normalize"] "setspolynomial_simplify_ok") let coq_setpolynomial_simplify_ok = - lazy (constant ["ring";"Ring_normalize"] "setpolynomial_simplify_ok") + lazy (constant ["ring";"Setoid_ring_normalize"] "setpolynomial_simplify_ok") (* Ring abstract *) let coq_ASPplus = lazy (constant ["ring";"Ring_abstract"] "ASPplus") @@ -648,9 +648,9 @@ let build_setpolynom gl th lc = mkLApp(coq_setpolynomial_simplify_ok, [| th.th_a; (unbox th.th_equiv); th.th_plus; th.th_mult; th.th_one; th.th_zero;(unbox th.th_opp); - th.th_eq; v; th.th_t; (unbox th.th_setoid_th); + th.th_eq; (unbox th.th_setoid_th); (unbox th.th_morph).plusm; (unbox th.th_morph).multm; - (unbox (unbox th.th_morph).oppm); p |]))) + (unbox (unbox th.th_morph).oppm); v; th.th_t; p |]))) lp (* -- cgit v1.2.3