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.
---
 .../user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh
new file mode 100644
index 0000000000..08112d3054
--- /dev/null
+++ b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "8902" ] || [ "$CI_BRANCH" = "ltac+use_atts_in_ast" ]; then
+
+    aactactics_CI_REF=ltac+use_atts_in_ast
+    aactactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
+
+    coqhammer_CI_REF=ltac+use_atts_in_ast
+    coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer
+
+    Equations_CI_REF=ltac+use_atts_in_ast
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    mtac2_CI_REF=ltac+use_atts_in_ast
+    mtac2_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
-- 
cgit v1.2.3