diff options
| author | Emilio Jesus Gallego Arias | 2017-01-17 15:45:43 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-24 23:58:23 +0200 |
| commit | 84eb5cd72a015c45337a5a6070c5651f56be6e74 (patch) | |
| tree | 6a54fa82bd711f37fa21f56dcce4591f9474b55c /plugins/setoid_ring | |
| parent | bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 (diff) | |
[location] Use located in tactics.
One case missing due the TACTIC EXTEND macro.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index bef8139bef..e3e14bcf35 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -161,11 +161,11 @@ 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) = @@ -580,8 +580,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 @@ -602,8 +602,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.ghost,TacCall(Loc.tag (t,[]))), plapp evd coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with |