diff options
| author | Pierre-Marie Pédrot | 2017-08-05 17:14:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-07 14:52:28 +0200 |
| commit | 77150cc524f5cbdc9bf340be03f31e7f7542c98d (patch) | |
| tree | 2b8741ef1386cea64d93d266d6eb4b7beab3757f /src/tac2expr.mli | |
| parent | 6e6f348958cc333040991ca3dc2525a7c91dc9c0 (diff) | |
Introducing grammar-free tactic notations.
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 7 |
1 files changed, 6 insertions, 1 deletions
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 |