From 4949b991019dd6dd845627cc03e800072bc7ed10 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 5 Nov 2018 02:51:23 +0100
Subject: [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.
---
 plugins/firstorder/g_ground.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 1128a78093..a212d13453 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -66,7 +66,7 @@ let default_intuition_tac =
   let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
   let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
   Tacenv.register_ml_tactic name [| tac |];
-  Tacexpr.TacML (Loc.tag (entry, []))
+  Tacexpr.TacML (CAst.make (entry, []))
 
 let (set_default_solver, default_solver, print_default_solver) = 
   Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
-- 
cgit v1.2.3