From 77150cc524f5cbdc9bf340be03f31e7f7542c98d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 5 Aug 2017 17:14:21 +0200
Subject: Introducing grammar-free tactic notations.

---
 src/tac2expr.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'src/tac2expr.mli')

diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 10d8c1d421..7efb85cbb0 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -18,10 +18,15 @@ type lid = Id.t
 type uid = Id.t
 
 type ltac_constant = KerName.t
+type ltac_alias = KerName.t
 type ltac_constructor = KerName.t
 type ltac_projection = KerName.t
 type type_constant = KerName.t
 
+type tacref =
+| TacConstant of ltac_constant
+| TacAlias of ltac_alias
+
 type 'a or_relid =
 | RelId of qualid located
 | AbsKn of 'a
@@ -88,7 +93,7 @@ type raw_patexpr =
 
 type raw_tacexpr =
 | CTacAtm of atom located
-| CTacRef of ltac_constant or_relid
+| CTacRef of tacref or_relid
 | CTacCst of Loc.t * ltac_constructor or_tuple or_relid
 | CTacFun of Loc.t * (raw_patexpr * raw_typexpr option) list * raw_tacexpr
 | CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list
-- 
cgit v1.2.3