aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml47
1 files changed, 24 insertions, 23 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 6b8ef630a2..cca5cde155 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -8,7 +8,6 @@
open Ltac_plugin
open Pp
-open CErrors
open Util
open Names
open Term
@@ -32,6 +31,8 @@ open Misctypes
open Newring_ast
open Proofview.Notations
+let error msg = CErrors.user_err Pp.(str msg)
+
(****************************************************************************)
(* controlled reduction *)
@@ -46,7 +47,7 @@ let tag_arg tag_rec map subs i c =
let global_head_of_constr sigma c =
let f, args = decompose_app sigma c in
try fst (Termops.global_of_constr sigma f)
- with Not_found -> anomaly (str "global_head_of_constr")
+ with Not_found -> CErrors.anomaly (str "global_head_of_constr.")
let global_of_constr_nofail c =
try global_of_constr c
@@ -82,7 +83,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps
let lookup_map map =
try String.Map.find map !protect_maps
with Not_found ->
- user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
+ CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
let protect_red map env sigma c0 =
let evars ev = Evarutil.safe_evar_value sigma ev in
@@ -127,11 +128,11 @@ let closed_term_ast l =
mltac_name = tacname;
mltac_index = 0;
} in
- let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
+ let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
TacFun([Name(Id.of_string"t")],
- TacML(Loc.ghost,tacname,
- [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
- TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))
+ TacML(Loc.tag (tacname,
+ [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None));
+ TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
*)
@@ -160,16 +161,16 @@ let decl_constant na ctx c =
(* Calling a global tactic *)
let ltac_call tac (args:glob_tactic_arg list) =
- TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args))
+ TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args)))
(* Calling a locally bound tactic *)
let ltac_lcall tac args =
- TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args))
+ TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar(Loc.tag @@ Id.of_string tac),args)))
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
+ let x = Reference (ArgVar (Loc.tag 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
@@ -204,7 +205,7 @@ let get_res =
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
+ let x = Reference (ArgVar (Loc.tag 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
@@ -212,7 +213,7 @@ let exec_tactic env evd n f args =
(** Build the getter *)
let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
- let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in
+ let get_res = TacML (Loc.tag (get_res, [TacGeneric n])) in
let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
(** Evaluate the whole result *)
let gl = dummy_goal env evd in
@@ -229,7 +230,7 @@ let stdlib_modules =
]
let coq_constant c =
- lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c))
+ lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
let coq_reference c =
lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
@@ -274,7 +275,7 @@ let plugin_modules =
]
let my_constant c =
- lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" plugin_modules c))
+ lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
let my_reference c =
lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
@@ -283,7 +284,7 @@ let znew_ring_path =
let zltac s =
lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s))
-let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);;
+let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);;
let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
(* Ring theory *)
@@ -359,13 +360,13 @@ let find_ring_structure env sigma l =
let check c =
let ty' = Retyping.get_type_of env sigma c in
if not (Reductionops.is_conv env sigma ty ty') then
- user_err ~hdr:"ring"
+ CErrors.user_err ~hdr:"ring"
(str"arguments of ring_simplify do not have all the same type")
in
List.iter check cl';
(try ring_for_carrier (EConstr.to_constr sigma ty)
with Not_found ->
- user_err ~hdr:"ring"
+ CErrors.user_err ~hdr:"ring"
(str"cannot find a declared ring structure over"++
spc()++str"\""++pr_constr ty++str"\""))
| [] -> assert false
@@ -577,8 +578,8 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
| Some (Closed lc) ->
closed_term_ast (List.map Smartlocate.global_with_alias lc)
| None ->
- let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in
- TacArg(Loc.ghost,TacCall(Loc.ghost,t,[]))
+ let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in
+ TacArg(Loc.tag (TacCall(Loc.tag (t,[]))))
let make_hyp env evd c =
let t = Retyping.get_type_of env !evd c in
@@ -599,8 +600,8 @@ let interp_power env evd pow =
let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
match pow with
| None ->
- let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in
- (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|])
+ let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
+ (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|])
| Some (tac, spec) ->
let tac =
match tac with
@@ -852,13 +853,13 @@ let find_field_structure env sigma l =
let check c =
let ty' = Retyping.get_type_of env sigma c in
if not (Reductionops.is_conv env sigma ty ty') then
- user_err ~hdr:"field"
+ CErrors.user_err ~hdr:"field"
(str"arguments of field_simplify do not have all the same type")
in
List.iter check cl';
(try field_for_carrier (EConstr.to_constr sigma ty)
with Not_found ->
- user_err ~hdr:"field"
+ CErrors.user_err ~hdr:"field"
(str"cannot find a declared field structure over"++
spc()++str"\""++pr_constr ty++str"\""))
| [] -> assert false
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 04:28:01 +0000