diff options
| author | Pierre-Marie Pédrot | 2016-02-22 10:32:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-22 16:29:04 +0100 |
| commit | f358d7b4c962f5288ad9ce2dc35802666c882422 (patch) | |
| tree | 3c5a27500644aa83de13e30740e330006448c2cd /plugins/setoid_ring | |
| parent | c5d0aa889fa80404f6c291000938e443d6200e5b (diff) | |
The tactic generic argument now returns a value rather than a glob_expr.
The glob_expr was actually always embedded as a VFun, so this patch should
not change anything semantically. The only change occurs in the plugin API
where one should use the Tacinterp.tactic_of_value function instead of
Tacinterp.eval_tactic.
Moreover, this patch allows to use tactics returning arguments from the ML
side.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 13 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.mli | 4 |
2 files changed, 7 insertions, 10 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index a67cc7cb87..37a8959767 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -176,19 +176,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: Tacinterp.Value.t list) = +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_letin ("F", Tacexp f) (ltac_lcall "F" args)) + Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args) let ltac_record flds = TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) @@ -774,7 +771,7 @@ let ltac_ring_structure e = [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] -let ring_lookup (f:glob_tactic_expr) lH rl t = +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 @@ -1046,7 +1043,7 @@ let ltac_field_structure e = [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 = +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 diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 4bd3383d65..07a1ae833b 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -45,7 +45,7 @@ val ic : constr_expr -> Evd.evar_map * constr val from_name : ring_info Spmap.t ref val ring_lookup : - glob_tactic_expr -> + Genarg.Val.t -> constr list -> constr list -> constr -> unit Proofview.tactic @@ -73,6 +73,6 @@ val add_field_theory : val field_from_name : field_info Spmap.t ref val field_lookup : - glob_tactic_expr -> + Genarg.Val.t -> constr list -> constr list -> constr -> unit Proofview.tactic |