diff options
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 33 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 1 |
3 files changed, 22 insertions, 18 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 142257bc80..afee6ff60d 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -198,20 +198,31 @@ 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 = Genarg.out_gen (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 args = List.map carg args in 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, [n]) in + let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(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"]; @@ -652,7 +663,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 @@ -937,7 +948,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 diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2597606aa1..1928b44b47 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2389,12 +2389,6 @@ let interp_redexp env sigma r = (* Embed tactics in raw or glob tactic expr *) let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t)) -let tacticIn t = - globTacticIn (fun ist -> - try glob_tactic (t ist) - with e when Errors.noncritical e -> anomaly ~label:"tacticIn" - (str "Incorrect tactic expression. Received exception is:" ++ - Errors.print e)) (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 60f1a47492..60c9dc43e4 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -46,7 +46,6 @@ val extract_ltac_constr_values : interp_sign -> Environ.env -> a [constr]. *) (** To embed several objects in Coqast.t *) -val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr val valueIn : value -> raw_tactic_arg |