diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 8 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 24 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_plugin.mllib | 3 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_plugin.mlpack | 2 |
4 files changed, 13 insertions, 24 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index f5a7340487..f64226e334 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -60,9 +60,9 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF 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:"); + Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> - msg_notice (hov 2 + 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)) @@ -89,9 +89,9 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF 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:"); + Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> - msg_notice (hov 2 + 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)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 271bf35a88..57ef920325 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -34,15 +34,6 @@ 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 = @@ -75,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 @@ -106,6 +95,7 @@ let protect_tac_in map id = (****************************************************************************) 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()) @@ -527,7 +517,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++ @@ -536,7 +526,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 \""++ diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib deleted file mode 100644 index 7d6c495889..0000000000 --- a/plugins/setoid_ring/newring_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Newring -Newring_plugin_mod -G_newring diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack new file mode 100644 index 0000000000..23663b4090 --- /dev/null +++ b/plugins/setoid_ring/newring_plugin.mlpack @@ -0,0 +1,2 @@ +Newring +G_newring |