diff options
| author | Emilio Jesus Gallego Arias | 2018-11-05 02:51:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 05:29:50 +0100 |
| commit | 4949b991019dd6dd845627cc03e800072bc7ed10 (patch) | |
| tree | 6d77ed011a33e2afdcd544ff301aa84a2056f9d2 /plugins/ltac/rewrite.ml | |
| parent | f8a76b3d383abf468fb21df509f5da8f8aafa913 (diff) | |
[ltac] Use CAst nodes in the tactic AST.
This provides several advantages to people serializing tactic
scripts. Appearance of the involved constructors is common enough as
to bother to submit this PR.
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 7d917c58fe..16cb75ea2f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1958,7 +1958,7 @@ let add_setoid atts binders a aeq t n = let make_tactic name = let open Tacexpr in let tacqid = Libnames.qualid_of_string name in - TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, [])))) + TacArg (CAst.make @@ (TacCall (CAst.make (tacqid, [])))) let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> |